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  2444  nelneq  2868  nelneq2  2869  r19.35  3114  nssne1  4071  nssne2  4072  psssstr  4132  prproe  4929  iununi  5122  disjiun  5154  nbrne1  5185  nbrne2  5186  propeqop  5526  mosubopt  5529  relsnb  5826  relcnvtrg  6297  reuop  6324  dfpo2  6327  tz7.7  6421  suctr  6481  tz6.12i  6948  ssimaex  7007  chfnrn  7082  fvn0ssdmfun  7108  ffnfv  7153  f1elima  7300  elovmpt3rab1  7710  limsssuc  7887  nnsuc  7921  peano5  7932  peano5OLD  7933  dftpos4  8286  odi  8635  pssnn  9234  fineqvlem  9325  ordunifi  9354  wdom2d  9649  r1pwss  9853  alephval3  10179  infdif  10277  cff1  10327  cofsmo  10338  axdc3lem2  10520  zorn2lem6  10570  cfpwsdom  10653  prub  11063  prnmadd  11066  1re  11290  letr  11384  dedekindle  11454  addrid  11470  negf1o  11720  negfi  12244  xrletr  13220  0fz1  13604  elfzmlbp  13696  leisorel  14509  elss2prb  14537  exprelprel  14539  fi1uzind  14556  swrdnd  14702  sqrmo  15300  isprm2  16729  nprmdvds1  16753  oddprmdvds  16950  catsubcat  17903  funcestrcsetclem8  18216  funcestrcsetclem9  18217  fthestrcsetc  18219  fullestrcsetc  18220  funcsetcestrclem9  18232  fthsetcestrc  18234  fullsetcestrc  18235  pltletr  18413  mgmpropd  18689  issstrmgm  18691  mgm2nsgrplem3  18955  sgrp2nmndlem3  18960  fvcosymgeq  19471  sylow2alem2  19660  rngcinv  20659  srhmsubc  20702  islss  20955  gzrngunitlem  21473  pjdm2  21754  assamulgscmlem2  21943  gsumply1subr  22256  dmatmul  22524  decpmatmullem  22798  monmat2matmon  22851  chpscmat  22869  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  isclo2  23117  fbasfip  23897  ufileu  23948  alexsubALTlem2  24077  cnextcn  24096  metustbl  24600  scutbdaybnd2lim  27880  addsprop  28027  elntg2  29018  ushgredgedg  29264  ushgredgedgloop  29266  edgnbusgreu  29402  nb3grprlem1  29415  cusgrfilem1  29491  cusgrfilem2  29492  umgr2v2evtxel  29558  wlkcompim  29668  usgr2pth  29800  usgr2trlncrct  29839  wwlknp  29876  wlkiswwlks2lem3  29904  wlkiswwlksupgr2  29910  wlklnwwlkln2lem  29915  wwlksnext  29926  2pthdlem1  29963  umgr2adedgwlkonALT  29980  umgr2wlkon  29983  elwspths2spth  30000  rusgr0edg  30006  clwlkclwwlklem2a1  30024  clwlkclwwlklem2a  30030  clwwisshclwwslem  30046  loopclwwlkn1b  30074  clwwlkel  30078  clwwlkext2edg  30088  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  clwwlknonwwlknonb  30138  uhgr3cyclexlem  30213  upgr4cycl4dv4e  30217  eupth2lem3lem4  30263  frgruhgr0v  30296  numclwwlk1lem2f1  30389  numclwlk2lem2f  30409  numclwlk2lem2f1o  30411  frgrogt3nreg  30429  5oalem6  31691  eigorthi  31869  adjbd1o  32117  dmdbr7ati  32456  ssdifidlprm  33451  fmla1  35355  satffunlem2lem2  35374  fundmpss  35730  funbreq  35733  idinside  36048  bj-opelidres  37127  bj-eldiag2  37143  bj-fvimacnv0  37252  poimirlem32  37612  sdclem2  37702  fdc1  37706  ismgmOLD  37810  lsatcvatlem  39005  atnle  39273  cvratlem  39378  ispsubcl2N  39904  trlord  40526  diaelrnN  41002  cdlemm10N  41075  dochexmidlem7  41423  fsuppind  42545  3impexpbicom  44450  sbcim2g  44509  suctrALT2VD  44807  suctrALT2  44808  3impexpVD  44827  3impexpbicomVD  44828  sbcim2gVD  44846  csbeq2gVD  44863  csbsngVD  44864  ax6e2ndeqVD  44880  2sb5ndVD  44881  infxrunb3rnmpt  45343  lptioo2  45552  lptioo1  45553  funressnfv  46958  ffnafv  47086  tz6.12i-afv2  47158  iccpartiltu  47296  iccpartigtl  47297  icceuelpartlem  47309  fargshiftfo  47316  ichnreuop  47346  reupr  47396  bgoldbtbndlem2  47680  uspgrlimlem1  47812  rngcinvALTV  47999  srhmsubcALTV  48048  nnolog2flm1  48324  prelrrx2b  48448  rrxlinec  48470  eenglngeehlnm  48473