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  2468  nelneq  2887  nelneq2  2888  r19.35  3123  nssne1  3999  nssne2  4000  psssstr  4064  prproe  4870  iununi  5065  disjiun  5097  nbrne1  5130  nbrne2  5131  propeqop  5490  mosubopt  5493  relsnb  5789  relcnvtrg  6268  reuop  6294  dfpo2  6297  tz7.7  6386  suctr  6449  tz6.12i  6907  ssimaex  6966  chfnrn  7044  fvn0ssdmfun  7069  ffnfv  7114  f1elima  7261  elovmpt3rab1  7670  limsssuc  7842  nnsuc  7876  peano5  7886  dftpos4  8237  odi  8560  pssnn  9149  fineqvlem  9222  ordunifi  9246  wdom2d  9538  r1pwss  9752  alephval3  10090  infdif  10187  cff1  10237  cofsmo  10248  axdc3lem2  10430  zorn2lem6  10480  cfpwsdom  10564  prub  10974  prnmadd  10977  1re  11203  letr  11299  dedekindle  11369  addrid  11385  negf1o  11639  negfi  12159  xrletr  13178  0fz1  13567  elfzmlbp  13663  leisorel  14493  elss2prb  14521  exprelprel  14523  fi1uzind  14540  swrdnd  14688  sqrmo  15298  isprm2  16735  nprmdvds1  16760  oddprmdvds  16958  catsubcat  17891  funcestrcsetclem8  18198  funcestrcsetclem9  18199  fthestrcsetc  18201  fullestrcsetc  18202  funcsetcestrclem9  18214  fthsetcestrc  18216  fullsetcestrc  18217  pltletr  18392  mgmpropd  18704  issstrmgm  18706  mgm2nsgrplem3  18977  sgrp2nmndlem3  18982  fvcosymgeq  19494  sylow2alem2  19683  rngcinv  20736  srhmsubc  20779  islss  21055  ssdifidlprm  21486  gzrngunitlem  21582  pjdm2  21861  assamulgscmlem2  22050  gsumply1subr  22393  dmatmul  22654  decpmatmullem  22928  monmat2matmon  22981  chpscmat  22999  chfacfscmulgsum  23017  chfacfpmmulgsum  23021  isclo2  23245  fbasfip  24025  ufileu  24076  alexsubALTlem2  24205  cnextcn  24224  metustbl  24723  cutbdaybnd2lim  27990  addsprop  28169  elntg2  29335  ushgredgedg  29579  ushgredgedgloop  29581  edgnbusgreu  29717  nb3grprlem1  29730  cusgrfilem1  29805  cusgrfilem2  29806  umgr2v2evtxel  29872  wlkcompim  29981  usgr2pth  30113  usgr2trlncrct  30155  wwlknp  30192  wlkiswwlks2lem3  30220  wlkiswwlksupgr2  30226  wlklnwwlkln2lem  30231  wwlksnext  30242  2pthdlem1  30279  umgr2adedgwlkonALT  30296  umgr2wlkon  30299  elwspths2spth  30319  rusgr0edg  30325  clwlkclwwlklem2a1  30343  clwlkclwwlklem2a  30349  clwwisshclwwslem  30365  loopclwwlkn1b  30393  clwwlkel  30397  clwwlkext2edg  30407  hashecclwwlkn1  30428  umgrhashecclwwlk  30429  clwwlknonwwlknonb  30457  uhgr3cyclexlem  30532  upgr4cycl4dv4e  30536  eupth2lem3lem4  30582  frgruhgr0v  30615  numclwwlk1lem2f1  30708  numclwlk2lem2f  30728  numclwlk2lem2f1o  30730  frgrogt3nreg  30748  5oalem6  32011  eigorthi  32189  adjbd1o  32437  dmdbr7ati  32776  fmla1  35879  satffunlem2lem2  35898  fundmpss  36259  funbreq  36262  idinside  36576  tr0elw  36995  tr0el  36996  dfttc4  37041  bj-opelidres  37805  bj-eldiag2  37821  bj-fvimacnv0  37930  wl-eujustlem1  38243  poimirlem32  38303  sdclem2  38393  fdc1  38397  ismgmOLD  38501  lsatcvatlem  39823  atnle  40091  cvratlem  40195  ispsubcl2N  40721  trlord  41343  diaelrnN  41819  cdlemm10N  41892  dochexmidlem7  42240  fsuppind  43322  3impexpbicom  45189  sbcim2g  45247  suctrALT2VD  45544  suctrALT2  45545  3impexpVD  45564  3impexpbicomVD  45565  sbcim2gVD  45583  csbeq2gVD  45600  csbsngVD  45601  ax6e2ndeqVD  45617  2sb5ndVD  45618  infxrunb3rnmpt  46142  lptioo2  46347  lptioo1  46348  funressnfv  47780  ffnafv  47908  tz6.12i-afv2  47980  iccpartiltu  48171  iccpartigtl  48172  icceuelpartlem  48184  fargshiftfo  48191  ichnreuop  48221  reupr  48271  bgoldbtbndlem2  48571  isubgredg  48631  upgrimtrlslem2  48670  cycl3grtrilem  48711  uspgrlimlem1  48753  grlimprclnbgrvtx  48764  gpgedg2ov  48831  gpgedg2iv  48832  rngcinvALTV  49041  srhmsubcALTV  49090  nnolog2flm1  49370  prelrrx2b  49494  rrxlinec  49516  eenglngeehlnm  49519