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  2440  nelneq  2860  nelneq2  2861  r19.35  3094  nssne1  3996  nssne2  3997  psssstr  4061  prproe  4861  iununi  5054  disjiun  5086  nbrne1  5117  nbrne2  5118  propeqop  5455  mosubopt  5458  relsnb  5751  relcnvtrg  6225  reuop  6251  dfpo2  6254  tz7.7  6343  suctr  6405  tz6.12i  6860  ssimaex  6919  chfnrn  6994  fvn0ssdmfun  7019  ffnfv  7064  f1elima  7209  elovmpt3rab1  7618  limsssuc  7792  nnsuc  7826  peano5  7835  dftpos4  8187  odi  8506  pssnn  9093  fineqvlem  9166  ordunifi  9190  wdom2d  9485  r1pwss  9696  alephval3  10020  infdif  10118  cff1  10168  cofsmo  10179  axdc3lem2  10361  zorn2lem6  10411  cfpwsdom  10495  prub  10905  prnmadd  10908  1re  11132  letr  11227  dedekindle  11297  addrid  11313  negf1o  11567  negfi  12091  xrletr  13072  0fz1  13460  elfzmlbp  13555  leisorel  14383  elss2prb  14411  exprelprel  14413  fi1uzind  14430  swrdnd  14578  sqrmo  15174  isprm2  16609  nprmdvds1  16633  oddprmdvds  16831  catsubcat  17763  funcestrcsetclem8  18070  funcestrcsetclem9  18071  fthestrcsetc  18073  fullestrcsetc  18074  funcsetcestrclem9  18086  fthsetcestrc  18088  fullsetcestrc  18089  pltletr  18264  mgmpropd  18576  issstrmgm  18578  mgm2nsgrplem3  18845  sgrp2nmndlem3  18850  fvcosymgeq  19358  sylow2alem2  19547  rngcinv  20570  srhmsubc  20613  islss  20885  gzrngunitlem  21387  pjdm2  21666  assamulgscmlem2  21856  gsumply1subr  22174  dmatmul  22441  decpmatmullem  22715  monmat2matmon  22768  chpscmat  22786  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  isclo2  23032  fbasfip  23812  ufileu  23863  alexsubALTlem2  23992  cnextcn  24011  metustbl  24510  cutbdaybnd2lim  27793  addsprop  27972  elntg2  29058  ushgredgedg  29302  ushgredgedgloop  29304  edgnbusgreu  29440  nb3grprlem1  29453  cusgrfilem1  29529  cusgrfilem2  29530  umgr2v2evtxel  29596  wlkcompim  29705  usgr2pth  29837  usgr2trlncrct  29879  wwlknp  29916  wlkiswwlks2lem3  29944  wlkiswwlksupgr2  29950  wlklnwwlkln2lem  29955  wwlksnext  29966  2pthdlem1  30003  umgr2adedgwlkonALT  30020  umgr2wlkon  30023  elwspths2spth  30043  rusgr0edg  30049  clwlkclwwlklem2a1  30067  clwlkclwwlklem2a  30073  clwwisshclwwslem  30089  loopclwwlkn1b  30117  clwwlkel  30121  clwwlkext2edg  30131  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  clwwlknonwwlknonb  30181  uhgr3cyclexlem  30256  upgr4cycl4dv4e  30260  eupth2lem3lem4  30306  frgruhgr0v  30339  numclwwlk1lem2f1  30432  numclwlk2lem2f  30452  numclwlk2lem2f1o  30454  frgrogt3nreg  30472  5oalem6  31734  eigorthi  31912  adjbd1o  32160  dmdbr7ati  32499  ssdifidlprm  33539  fmla1  35581  satffunlem2lem2  35600  fundmpss  35961  funbreq  35964  idinside  36278  bj-opelidres  37366  bj-eldiag2  37382  bj-fvimacnv0  37491  wl-eujustlem1  37793  poimirlem32  37853  sdclem2  37943  fdc1  37947  ismgmOLD  38051  lsatcvatlem  39309  atnle  39577  cvratlem  39681  ispsubcl2N  40207  trlord  40829  diaelrnN  41305  cdlemm10N  41378  dochexmidlem7  41726  fsuppind  42833  3impexpbicom  44721  sbcim2g  44779  suctrALT2VD  45076  suctrALT2  45077  3impexpVD  45096  3impexpbicomVD  45097  sbcim2gVD  45115  csbeq2gVD  45132  csbsngVD  45133  ax6e2ndeqVD  45149  2sb5ndVD  45150  infxrunb3rnmpt  45672  lptioo2  45877  lptioo1  45878  funressnfv  47289  ffnafv  47417  tz6.12i-afv2  47489  iccpartiltu  47668  iccpartigtl  47669  icceuelpartlem  47681  fargshiftfo  47688  ichnreuop  47718  reupr  47768  bgoldbtbndlem2  48052  isubgredg  48112  upgrimtrlslem2  48151  cycl3grtrilem  48192  uspgrlimlem1  48234  grlimprclnbgrvtx  48245  gpgedg2ov  48312  gpgedg2iv  48313  rngcinvALTV  48522  srhmsubcALTV  48571  nnolog2flm1  48836  prelrrx2b  48960  rrxlinec  48982  eenglngeehlnm  48985