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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  biimpac  483  axc16i  2474  nelneq  2893  nelneq2  2894  r19.35  3129  nssne1  4007  nssne2  4008  psssstr  4072  prproe  4874  iununi  5069  disjiun  5101  nbrne1  5134  nbrne2  5135  propeqop  5491  mosubopt  5494  relsnb  5790  relcnvtrg  6269  reuop  6295  dfpo2  6298  tz7.7  6387  suctr  6450  tz6.12i  6908  ssimaex  6967  chfnrn  7045  fvn0ssdmfun  7070  ffnfv  7115  f1elima  7262  elovmpt3rab1  7671  limsssuc  7845  nnsuc  7879  peano5  7889  dftpos4  8240  odi  8563  pssnn  9152  fineqvlem  9225  ordunifi  9249  wdom2d  9541  r1pwss  9755  alephval3  10093  infdif  10190  cff1  10241  cofsmo  10252  axdc3lem2  10434  zorn2lem6  10484  cfpwsdom  10568  prub  10978  prnmadd  10981  1re  11207  letr  11303  dedekindle  11373  addrid  11389  negf1o  11643  negfi  12163  xrletr  13182  0fz1  13571  elfzmlbp  13666  leisorel  14496  elss2prb  14524  exprelprel  14526  fi1uzind  14543  swrdnd  14691  sqrmo  15301  isprm2  16739  nprmdvds1  16764  oddprmdvds  16962  catsubcat  17895  funcestrcsetclem8  18202  funcestrcsetclem9  18203  fthestrcsetc  18205  fullestrcsetc  18206  funcsetcestrclem9  18218  fthsetcestrc  18220  fullsetcestrc  18221  pltletr  18396  mgmpropd  18708  issstrmgm  18710  mgm2nsgrplem3  18981  sgrp2nmndlem3  18986  fvcosymgeq  19498  sylow2alem2  19687  rngcinv  20721  srhmsubc  20764  islss  21032  ssdifidlprm  21454  gzrngunitlem  21550  pjdm2  21829  assamulgscmlem2  22018  gsumply1subr  22361  dmatmul  22622  decpmatmullem  22896  monmat2matmon  22949  chpscmat  22967  chfacfscmulgsum  22985  chfacfpmmulgsum  22989  isclo2  23213  fbasfip  23993  ufileu  24044  alexsubALTlem2  24173  cnextcn  24192  metustbl  24691  cutbdaybnd2lim  27955  addsprop  28134  elntg2  29275  ushgredgedg  29519  ushgredgedgloop  29521  edgnbusgreu  29657  nb3grprlem1  29670  cusgrfilem1  29745  cusgrfilem2  29746  umgr2v2evtxel  29812  wlkcompim  29921  usgr2pth  30053  usgr2trlncrct  30095  wwlknp  30132  wlkiswwlks2lem3  30160  wlkiswwlksupgr2  30166  wlklnwwlkln2lem  30171  wwlksnext  30182  2pthdlem1  30219  umgr2adedgwlkonALT  30236  umgr2wlkon  30239  elwspths2spth  30259  rusgr0edg  30265  clwlkclwwlklem2a1  30283  clwlkclwwlklem2a  30289  clwwisshclwwslem  30305  loopclwwlkn1b  30333  clwwlkel  30337  clwwlkext2edg  30347  hashecclwwlkn1  30368  umgrhashecclwwlk  30369  clwwlknonwwlknonb  30397  uhgr3cyclexlem  30472  upgr4cycl4dv4e  30476  eupth2lem3lem4  30522  frgruhgr0v  30555  numclwwlk1lem2f1  30648  numclwlk2lem2f  30668  numclwlk2lem2f1o  30670  frgrogt3nreg  30688  5oalem6  31951  eigorthi  32129  adjbd1o  32377  dmdbr7ati  32716  fmla1  35777  satffunlem2lem2  35796  fundmpss  36157  funbreq  36160  idinside  36474  tr0elw  36883  tr0el  36884  dfttc4  36929  bj-opelidres  37692  bj-eldiag2  37708  bj-fvimacnv0  37817  wl-eujustlem1  38130  poimirlem32  38190  sdclem2  38280  fdc1  38284  ismgmOLD  38388  lsatcvatlem  39712  atnle  39980  cvratlem  40084  ispsubcl2N  40610  trlord  41232  diaelrnN  41708  cdlemm10N  41781  dochexmidlem7  42129  fsuppind  43213  3impexpbicom  45080  sbcim2g  45138  suctrALT2VD  45435  suctrALT2  45436  3impexpVD  45455  3impexpbicomVD  45456  sbcim2gVD  45474  csbeq2gVD  45491  csbsngVD  45492  ax6e2ndeqVD  45508  2sb5ndVD  45509  infxrunb3rnmpt  46033  lptioo2  46238  lptioo1  46239  funressnfv  47668  ffnafv  47796  tz6.12i-afv2  47868  iccpartiltu  48059  iccpartigtl  48060  icceuelpartlem  48072  fargshiftfo  48079  ichnreuop  48109  reupr  48159  bgoldbtbndlem2  48459  isubgredg  48519  upgrimtrlslem2  48558  cycl3grtrilem  48599  uspgrlimlem1  48641  grlimprclnbgrvtx  48652  gpgedg2ov  48719  gpgedg2iv  48720  rngcinvALTV  48929  srhmsubcALTV  48978  nnolog2flm1  49254  prelrrx2b  49378  rrxlinec  49400  eenglngeehlnm  49403