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  2466  nelneq  2885  nelneq2  2886  r19.35  3121  nssne1  3993  nssne2  3994  psssstr  4058  prproe  4865  iununi  5059  disjiun  5091  nbrne1  5124  nbrne2  5125  propeqop  5479  mosubopt  5482  mosubott  5484  relsnb  5780  relcnvtrgOLD  6269  reuop  6296  dfpo2  6299  tz7.7  6388  suctr  6451  tz6.12i  6911  ssimaex  6970  chfnrn  7048  fvn0ssdmfun  7074  ffnfv  7119  f1elima  7267  elovmpt3rab1  7681  limsssuc  7861  nnsuc  7895  peano5  7905  dftpos4  8262  odi  8587  pssnn  9184  fineqvlem  9257  ordunifi  9281  wdom2d  9574  r1pwss  9791  alephval3  10189  infdif  10286  cff1  10336  cofsmo  10347  axdc3lem2  10529  zorn2lem6  10579  cfpwsdom  10669  prub  11079  prnmadd  11082  1re  11308  letr  11404  dedekindle  11474  addrid  11490  negf1o  11746  negfi  12266  xrletr  13287  0fz1  13677  elfzmlbp  13773  leisorel  14605  elss2prb  14633  exprelprel  14635  fi1uzind  14652  swrdnd  14804  sqrmo  15418  isprm2  16857  nprmdvds1  16882  oddprmdvds  17081  catsubcat  18014  funcestrcsetclem8  18321  funcestrcsetclem9  18322  fthestrcsetc  18324  fullestrcsetc  18325  funcsetcestrclem9  18337  fthsetcestrc  18339  fullsetcestrc  18340  pltletr  18515  mgmpropd  18829  issstrmgm  18831  mgm2nsgrplem3  19119  sgrp2nmndlem3  19124  fvcosymgeq  19643  sylow2alem2  19832  rngcinv  20889  srhmsubc  20932  islss  21209  ssdifidlprm  21642  gzrngunitlem  21738  pjdm2  22017  assamulgscmlem2  22208  gsumply1subr  22551  dmatmul  22812  decpmatmullem  23089  monmat2matmon  23142  chpscmat  23160  chfacfscmulgsum  23178  chfacfpmmulgsum  23182  isclo2  23406  fbasfip  24187  ufileu  24238  alexsubALTlem2  24367  cnextcn  24386  metustbl  24885  cutbdaybnd2lim  28183  addsprop  28362  elntg2  29563  ushgredgedg  29810  ushgredgedgloop  29812  edgnbusgreu  29948  nb3grprlem1  29961  cusgrfilem1  30036  cusgrfilem2  30037  umgr2v2evtxel  30103  wlkcompim  30212  usgr2pth  30350  usgr2trlncrct  30395  wwlknp  30432  wlkiswwlks2lem3  30460  wlkiswwlksupgr2  30466  wlklnwwlkln2lem  30471  wwlksnext  30482  2pthdlem1  30519  umgr2adedgwlkonALT  30536  umgr2wlkon  30539  elwspths2spth  30559  rusgr0edg  30565  clwlkclwwlklem2a1  30583  clwlkclwwlklem2a  30589  clwwisshclwwslem  30605  loopclwwlkn1b  30633  clwwlkel  30637  clwwlkext2edg  30647  hashecclwwlkn1  30668  umgrhashecclwwlk  30669  clwwlknonwwlknonb  30697  uhgr3cyclexlem  30782  upgr4cycl4dv4e  30786  eupth2lem3lem4  30832  frgruhgr0v  30865  numclwwlk1lem2f1  30958  numclwlk2lem2f  30978  numclwlk2lem2f1o  30980  frgrogt3nreg  30998  5oalem6  32261  eigorthi  32439  adjbd1o  32687  dmdbr7ati  33026  acwer1prc  35760  fmla1  36152  satffunlem2lem2  36171  fundmpss  36532  funbreq  36534  idinside  36849  tr0elw  37272  tr0el  37273  dfttc4  37318  bj-opelidres  38082  bj-eldiag2  38098  bj-fvimacnv0  38207  wl-eujustlem1  38520  poimirlem32  38570  sdclem2  38676  fdc1  38680  ismgmOLD  38784  lsatcvatlem  40106  atnle  40374  cvratlem  40478  ispsubcl2N  41004  trlord  41626  diaelrnN  42102  cdlemm10N  42175  dochexmidlem7  42523  fsuppind  43618  3impexpbicom  45462  sbcim2g  45520  suctrALT2VD  45817  suctrALT2  45818  3impexpVD  45837  3impexpbicomVD  45838  sbcim2gVD  45856  csbeq2gVD  45873  csbsngVD  45874  ax6e2ndeqVD  45890  2sb5ndVD  45891  dmstructnn  45925  dmstructfi  45926  infxrunb3rnmpt  46437  lptioo2  46642  lptioo1  46643  funressnfv  48112  ffnafv  48240  tz6.12i-afv2  48312  iccpartiltu  48503  iccpartigtl  48504  icceuelpartlem  48516  fargshiftfo  48523  ichnreuop  48553  reupr  48603  bgoldbtbndlem2  48903  isubgredg  48963  upgrimtrlslem2  49002  cycl3grtrilem  49043  uspgrlimlem1  49085  grlimprclnbgrvtx  49096  gpgedg2ov  49163  gpgedg2iv  49164  rngcinvALTV  49372  srhmsubcALTV  49421  nnolog2flm1  49701  prelrrx2b  49825  rrxlinec  49847  eenglngeehlnm  49850