Theorem biimpcd 252

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 23	. 2 ⊢ (𝜓 → 𝜓)
2		biimpcd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	syl5ibcom 248	1 ⊢ (𝜓 → (𝜑 → 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biimpac  484  axc16i  2470  nelneq  2889  nelneq2  2890  r19.35  3125  nssne1  4000  nssne2  4001  psssstr  4065  prproe  4872  iununi  5067  disjiun  5099  nbrne1  5132  nbrne2  5133  propeqop  5492  mosubopt  5495  relsnb  5791  relcnvtrgOLD  6271  reuop  6298  dfpo2  6301  tz7.7  6390  suctr  6453  tz6.12i  6911  ssimaex  6970  chfnrn  7048  fvn0ssdmfun  7073  ffnfv  7118  f1elima  7266  elovmpt3rab1  7680  limsssuc  7852  nnsuc  7886  peano5  7896  dftpos4  8247  odi  8570  pssnn  9160  fineqvlem  9233  ordunifi  9257  wdom2d  9549  r1pwss  9763  alephval3  10110  infdif  10207  cff1  10257  cofsmo  10268  axdc3lem2  10450  zorn2lem6  10500  cfpwsdom  10584  prub  10994  prnmadd  10997  1re  11223  letr  11319  dedekindle  11389  addrid  11405  negf1o  11659  negfi  12179  xrletr  13199  0fz1  13588  elfzmlbp  13684  leisorel  14515  elss2prb  14543  exprelprel  14545  fi1uzind  14562  swrdnd  14714  sqrmo  15326  isprm2  16762  nprmdvds1  16787  oddprmdvds  16985  catsubcat  17918  funcestrcsetclem8  18225  funcestrcsetclem9  18226  fthestrcsetc  18228  fullestrcsetc  18229  funcsetcestrclem9  18241  fthsetcestrc  18243  fullsetcestrc  18244  pltletr  18419  mgmpropd  18733  issstrmgm  18735  mgm2nsgrplem3  19019  sgrp2nmndlem3  19024  fvcosymgeq  19543  sylow2alem2  19732  rngcinv  20786  srhmsubc  20829  islss  21105  ssdifidlprm  21536  gzrngunitlem  21632  pjdm2  21911  assamulgscmlem2  22100  gsumply1subr  22443  dmatmul  22704  decpmatmullem  22978  monmat2matmon  23031  chpscmat  23049  chfacfscmulgsum  23067  chfacfpmmulgsum  23071  isclo2  23295  fbasfip  24076  ufileu  24127  alexsubALTlem2  24256  cnextcn  24275  metustbl  24774  cutbdaybnd2lim  28041  addsprop  28220  elntg2  29390  ushgredgedg  29637  ushgredgedgloop  29639  edgnbusgreu  29775  nb3grprlem1  29788  cusgrfilem1  29863  cusgrfilem2  29864  umgr2v2evtxel  29930  wlkcompim  30039  usgr2pth  30177  usgr2trlncrct  30222  wwlknp  30259  wlkiswwlks2lem3  30287  wlkiswwlksupgr2  30293  wlklnwwlkln2lem  30298  wwlksnext  30309  2pthdlem1  30346  umgr2adedgwlkonALT  30363  umgr2wlkon  30366  elwspths2spth  30386  rusgr0edg  30392  clwlkclwwlklem2a1  30410  clwlkclwwlklem2a  30416  clwwisshclwwslem  30432  loopclwwlkn1b  30460  clwwlkel  30464  clwwlkext2edg  30474  hashecclwwlkn1  30495  umgrhashecclwwlk  30496  clwwlknonwwlknonb  30524  uhgr3cyclexlem  30603  upgr4cycl4dv4e  30607  eupth2lem3lem4  30653  frgruhgr0v  30686  numclwwlk1lem2f1  30779  numclwlk2lem2f  30799  numclwlk2lem2f1o  30801  frgrogt3nreg  30819  5oalem6  32082  eigorthi  32260  adjbd1o  32508  dmdbr7ati  32847  fmla1  35916  satffunlem2lem2  35935  fundmpss  36296  funbreq  36299  idinside  36613  tr0elw  37052  tr0el  37053  dfttc4  37098  bj-opelidres  37862  bj-eldiag2  37878  bj-fvimacnv0  37987  wl-eujustlem1  38300  poimirlem32  38360  sdclem2  38451  fdc1  38455  ismgmOLD  38559  lsatcvatlem  39881  atnle  40149  cvratlem  40253  ispsubcl2N  40779  trlord  41401  diaelrnN  41877  cdlemm10N  41950  dochexmidlem7  42298  fsuppind  43380  3impexpbicom  45247  sbcim2g  45305  suctrALT2VD  45602  suctrALT2  45603  3impexpVD  45622  3impexpbicomVD  45623  sbcim2gVD  45641  csbeq2gVD  45658  csbsngVD  45659  ax6e2ndeqVD  45675  2sb5ndVD  45676  infxrunb3rnmpt  46200  lptioo2  46405  lptioo1  46406  funressnfv  47838  ffnafv  47966  tz6.12i-afv2  48038  iccpartiltu  48229  iccpartigtl  48230  icceuelpartlem  48242  fargshiftfo  48249  ichnreuop  48279  reupr  48329  bgoldbtbndlem2  48629  isubgredg  48689  upgrimtrlslem2  48728  cycl3grtrilem  48769  uspgrlimlem1  48811  grlimprclnbgrvtx  48822  gpgedg2ov  48889  gpgedg2iv  48890  rngcinvALTV  49098  srhmsubcALTV  49147  nnolog2flm1  49427  prelrrx2b  49551  rrxlinec  49573  eenglngeehlnm  49576