Theorem biimpcd 249

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 245	1 ⊢ (𝜓 → (𝜑 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  biimpac  478  axc16i  2439  nelneq  2857  nelneq2  2858  r19.35  3095  nssne1  4028  nssne2  4029  psssstr  4091  prproe  4887  iununi  5081  disjiun  5113  nbrne1  5144  nbrne2  5145  propeqop  5494  mosubopt  5497  relsnb  5794  relcnvtrg  6268  reuop  6295  dfpo2  6298  tz7.7  6391  suctr  6451  tz6.12i  6915  ssimaex  6975  chfnrn  7050  fvn0ssdmfun  7075  ffnfv  7120  f1elima  7266  elovmpt3rab1  7676  limsssuc  7854  nnsuc  7888  peano5  7898  dftpos4  8253  odi  8600  pssnn  9191  fineqvlem  9281  ordunifi  9309  wdom2d  9603  r1pwss  9807  alephval3  10133  infdif  10231  cff1  10281  cofsmo  10292  axdc3lem2  10474  zorn2lem6  10524  cfpwsdom  10607  prub  11017  prnmadd  11020  1re  11244  letr  11338  dedekindle  11408  addrid  11424  negf1o  11676  negfi  12200  xrletr  13183  0fz1  13567  elfzmlbp  13662  leisorel  14482  elss2prb  14510  exprelprel  14512  fi1uzind  14529  swrdnd  14675  sqrmo  15273  isprm2  16702  nprmdvds1  16726  oddprmdvds  16924  catsubcat  17860  funcestrcsetclem8  18167  funcestrcsetclem9  18168  fthestrcsetc  18170  fullestrcsetc  18171  funcsetcestrclem9  18183  fthsetcestrc  18185  fullsetcestrc  18186  pltletr  18362  mgmpropd  18638  issstrmgm  18640  mgm2nsgrplem3  18907  sgrp2nmndlem3  18912  fvcosymgeq  19420  sylow2alem2  19609  rngcinv  20610  srhmsubc  20653  islss  20905  gzrngunitlem  21417  pjdm2  21698  assamulgscmlem2  21887  gsumply1subr  22202  dmatmul  22470  decpmatmullem  22744  monmat2matmon  22797  chpscmat  22815  chfacfscmulgsum  22833  chfacfpmmulgsum  22837  isclo2  23061  fbasfip  23841  ufileu  23892  alexsubALTlem2  24021  cnextcn  24040  metustbl  24542  scutbdaybnd2lim  27817  addsprop  27964  elntg2  28949  ushgredgedg  29193  ushgredgedgloop  29195  edgnbusgreu  29331  nb3grprlem1  29344  cusgrfilem1  29420  cusgrfilem2  29421  umgr2v2evtxel  29487  wlkcompim  29597  usgr2pth  29731  usgr2trlncrct  29773  wwlknp  29810  wlkiswwlks2lem3  29838  wlkiswwlksupgr2  29844  wlklnwwlkln2lem  29849  wwlksnext  29860  2pthdlem1  29897  umgr2adedgwlkonALT  29914  umgr2wlkon  29917  elwspths2spth  29934  rusgr0edg  29940  clwlkclwwlklem2a1  29958  clwlkclwwlklem2a  29964  clwwisshclwwslem  29980  loopclwwlkn1b  30008  clwwlkel  30012  clwwlkext2edg  30022  hashecclwwlkn1  30043  umgrhashecclwwlk  30044  clwwlknonwwlknonb  30072  uhgr3cyclexlem  30147  upgr4cycl4dv4e  30151  eupth2lem3lem4  30197  frgruhgr0v  30230  numclwwlk1lem2f1  30323  numclwlk2lem2f  30343  numclwlk2lem2f1o  30345  frgrogt3nreg  30363  5oalem6  31625  eigorthi  31803  adjbd1o  32051  dmdbr7ati  32390  ssdifidlprm  33427  fmla1  35333  satffunlem2lem2  35352  fundmpss  35708  funbreq  35711  idinside  36026  bj-opelidres  37103  bj-eldiag2  37119  bj-fvimacnv0  37228  poimirlem32  37600  sdclem2  37690  fdc1  37694  ismgmOLD  37798  lsatcvatlem  38991  atnle  39259  cvratlem  39364  ispsubcl2N  39890  trlord  40512  diaelrnN  40988  cdlemm10N  41061  dochexmidlem7  41409  fsuppind  42545  3impexpbicom  44445  sbcim2g  44503  suctrALT2VD  44801  suctrALT2  44802  3impexpVD  44821  3impexpbicomVD  44822  sbcim2gVD  44840  csbeq2gVD  44857  csbsngVD  44858  ax6e2ndeqVD  44874  2sb5ndVD  44875  infxrunb3rnmpt  45384  lptioo2  45591  lptioo1  45592  funressnfv  47001  ffnafv  47129  tz6.12i-afv2  47201  iccpartiltu  47355  iccpartigtl  47356  icceuelpartlem  47368  fargshiftfo  47375  ichnreuop  47405  reupr  47455  bgoldbtbndlem2  47739  isubgredg  47798  cycl3grtrilem  47859  uspgrlimlem1  47901  rngcinvALTV  48138  srhmsubcALTV  48187  nnolog2flm1  48457  prelrrx2b  48581  rrxlinec  48603  eenglngeehlnm  48606