Theorem biimpcd 248

Description: Deduce a commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)

Hypothesis

Ref	Expression
biimpcd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimpcd	⊢ (𝜓 → (𝜑 → 𝜒))

Proof of Theorem biimpcd

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2		biimpcd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	syl5ibcom 244	1 ⊢ (𝜓 → (𝜑 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  biimpac  478  axc16i  2430  nelneq  2852  nelneq2  2853  r19.35  3103  nssne1  4040  nssne2  4041  psssstr  4102  prproe  4901  iununi  5096  disjiun  5129  nbrne1  5161  nbrne2  5162  propeqop  5503  mosubopt  5506  relsnb  5798  relcnvtrg  6264  reuop  6291  dfpo2  6294  tz7.7  6389  suctr  6449  tz6.12i  6919  ssimaex  6977  chfnrn  7052  fvn0ssdmfun  7078  ffnfv  7123  f1elima  7267  elovmpt3rab1  7675  limsssuc  7848  nnsuc  7882  peano5  7893  peano5OLD  7894  dftpos4  8244  odi  8593  pssnn  9184  fineqvlem  9278  pssnnOLD  9281  ordunifi  9309  wdom2d  9595  r1pwss  9799  alephval3  10125  infdif  10224  cff1  10273  cofsmo  10284  axdc3lem2  10466  zorn2lem6  10516  cfpwsdom  10599  prub  11009  prnmadd  11012  1re  11236  letr  11330  dedekindle  11400  addrid  11416  negf1o  11666  negfi  12185  xrletr  13161  0fz1  13545  elfzmlbp  13636  leisorel  14445  elss2prb  14472  exprelprel  14474  fi1uzind  14482  swrdnd  14628  sqrmo  15222  isprm2  16644  nprmdvds1  16668  oddprmdvds  16863  catsubcat  17816  funcestrcsetclem8  18129  funcestrcsetclem9  18130  fthestrcsetc  18132  fullestrcsetc  18133  funcsetcestrclem9  18145  fthsetcestrc  18147  fullsetcestrc  18148  pltletr  18326  mgmpropd  18602  issstrmgm  18604  mgm2nsgrplem3  18863  sgrp2nmndlem3  18868  fvcosymgeq  19375  sylow2alem2  19564  rngcinv  20559  srhmsubc  20602  islss  20807  gzrngunitlem  21352  pjdm2  21632  assamulgscmlem2  21820  gsumply1subr  22139  dmatmul  22386  decpmatmullem  22660  monmat2matmon  22713  chpscmat  22731  chfacfscmulgsum  22749  chfacfpmmulgsum  22753  isclo2  22979  fbasfip  23759  ufileu  23810  alexsubALTlem2  23939  cnextcn  23958  metustbl  24462  scutbdaybnd2lim  27737  addsprop  27880  elntg2  28783  ushgredgedg  29029  ushgredgedgloop  29031  edgnbusgreu  29167  nb3grprlem1  29180  cusgrfilem1  29256  cusgrfilem2  29257  umgr2v2evtxel  29323  wlkcompim  29433  usgr2pth  29565  usgr2trlncrct  29604  wwlknp  29641  wlkiswwlks2lem3  29669  wlkiswwlksupgr2  29675  wlklnwwlkln2lem  29680  wwlksnext  29691  2pthdlem1  29728  umgr2adedgwlkonALT  29745  umgr2wlkon  29748  elwspths2spth  29765  rusgr0edg  29771  clwlkclwwlklem2a1  29789  clwlkclwwlklem2a  29795  clwwisshclwwslem  29811  loopclwwlkn1b  29839  clwwlkel  29843  clwwlkext2edg  29853  hashecclwwlkn1  29874  umgrhashecclwwlk  29875  clwwlknonwwlknonb  29903  uhgr3cyclexlem  29978  upgr4cycl4dv4e  29982  eupth2lem3lem4  30028  frgruhgr0v  30061  numclwwlk1lem2f1  30154  numclwlk2lem2f  30174  numclwlk2lem2f1o  30176  frgrogt3nreg  30194  5oalem6  31456  eigorthi  31634  adjbd1o  31882  dmdbr7ati  32221  fmla1  34933  satffunlem2lem2  34952  fundmpss  35298  funbreq  35301  idinside  35616  bj-opelidres  36576  bj-eldiag2  36592  bj-fvimacnv0  36701  poimirlem32  37060  sdclem2  37150  fdc1  37154  ismgmOLD  37258  lsatcvatlem  38458  atnle  38726  cvratlem  38831  ispsubcl2N  39357  trlord  39979  diaelrnN  40455  cdlemm10N  40528  dochexmidlem7  40876  fsuppind  41745  3impexpbicom  43841  sbcim2g  43900  suctrALT2VD  44198  suctrALT2  44199  3impexpVD  44218  3impexpbicomVD  44219  sbcim2gVD  44237  csbeq2gVD  44254  csbsngVD  44255  ax6e2ndeqVD  44271  2sb5ndVD  44272  infxrunb3rnmpt  44733  lptioo2  44942  lptioo1  44943  funressnfv  46348  ffnafv  46474  tz6.12i-afv2  46546  iccpartiltu  46685  iccpartigtl  46686  icceuelpartlem  46698  fargshiftfo  46705  ichnreuop  46735  reupr  46785  bgoldbtbndlem2  47069  rngcinvALTV  47261  srhmsubcALTV  47310  nnolog2flm1  47586  prelrrx2b  47710  rrxlinec  47732  eenglngeehlnm  47735