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  2434  nelneq  2852  nelneq2  2853  r19.35  3088  nssne1  4006  nssne2  4007  psssstr  4068  prproe  4865  iununi  5058  disjiun  5090  nbrne1  5121  nbrne2  5122  propeqop  5462  mosubopt  5465  relsnb  5756  relcnvtrg  6227  reuop  6254  dfpo2  6257  tz7.7  6346  suctr  6408  tz6.12i  6868  ssimaex  6928  chfnrn  7003  fvn0ssdmfun  7028  ffnfv  7073  f1elima  7220  elovmpt3rab1  7629  limsssuc  7806  nnsuc  7840  peano5  7849  dftpos4  8201  odi  8520  pssnn  9109  fineqvlem  9185  ordunifi  9213  wdom2d  9509  r1pwss  9713  alephval3  10039  infdif  10137  cff1  10187  cofsmo  10198  axdc3lem2  10380  zorn2lem6  10430  cfpwsdom  10513  prub  10923  prnmadd  10926  1re  11150  letr  11244  dedekindle  11314  addrid  11330  negf1o  11584  negfi  12108  xrletr  13094  0fz1  13481  elfzmlbp  13576  leisorel  14401  elss2prb  14429  exprelprel  14431  fi1uzind  14448  swrdnd  14595  sqrmo  15193  isprm2  16628  nprmdvds1  16652  oddprmdvds  16850  catsubcat  17781  funcestrcsetclem8  18088  funcestrcsetclem9  18089  fthestrcsetc  18091  fullestrcsetc  18092  funcsetcestrclem9  18104  fthsetcestrc  18106  fullsetcestrc  18107  pltletr  18282  mgmpropd  18560  issstrmgm  18562  mgm2nsgrplem3  18829  sgrp2nmndlem3  18834  fvcosymgeq  19343  sylow2alem2  19532  rngcinv  20557  srhmsubc  20600  islss  20872  gzrngunitlem  21374  pjdm2  21653  assamulgscmlem2  21842  gsumply1subr  22151  dmatmul  22417  decpmatmullem  22691  monmat2matmon  22744  chpscmat  22762  chfacfscmulgsum  22780  chfacfpmmulgsum  22784  isclo2  23008  fbasfip  23788  ufileu  23839  alexsubALTlem2  23968  cnextcn  23987  metustbl  24487  scutbdaybnd2lim  27763  addsprop  27923  elntg2  28965  ushgredgedg  29209  ushgredgedgloop  29211  edgnbusgreu  29347  nb3grprlem1  29360  cusgrfilem1  29436  cusgrfilem2  29437  umgr2v2evtxel  29503  wlkcompim  29612  usgr2pth  29744  usgr2trlncrct  29786  wwlknp  29823  wlkiswwlks2lem3  29851  wlkiswwlksupgr2  29857  wlklnwwlkln2lem  29862  wwlksnext  29873  2pthdlem1  29910  umgr2adedgwlkonALT  29927  umgr2wlkon  29930  elwspths2spth  29947  rusgr0edg  29953  clwlkclwwlklem2a1  29971  clwlkclwwlklem2a  29977  clwwisshclwwslem  29993  loopclwwlkn1b  30021  clwwlkel  30025  clwwlkext2edg  30035  hashecclwwlkn1  30056  umgrhashecclwwlk  30057  clwwlknonwwlknonb  30085  uhgr3cyclexlem  30160  upgr4cycl4dv4e  30164  eupth2lem3lem4  30210  frgruhgr0v  30243  numclwwlk1lem2f1  30336  numclwlk2lem2f  30356  numclwlk2lem2f1o  30358  frgrogt3nreg  30376  5oalem6  31638  eigorthi  31816  adjbd1o  32064  dmdbr7ati  32403  ssdifidlprm  33422  fmla1  35367  satffunlem2lem2  35386  fundmpss  35747  funbreq  35750  idinside  36065  bj-opelidres  37142  bj-eldiag2  37158  bj-fvimacnv0  37267  poimirlem32  37639  sdclem2  37729  fdc1  37733  ismgmOLD  37837  lsatcvatlem  39035  atnle  39303  cvratlem  39408  ispsubcl2N  39934  trlord  40556  diaelrnN  41032  cdlemm10N  41105  dochexmidlem7  41453  fsuppind  42571  3impexpbicom  44463  sbcim2g  44521  suctrALT2VD  44818  suctrALT2  44819  3impexpVD  44838  3impexpbicomVD  44839  sbcim2gVD  44857  csbeq2gVD  44874  csbsngVD  44875  ax6e2ndeqVD  44891  2sb5ndVD  44892  infxrunb3rnmpt  45417  lptioo2  45622  lptioo1  45623  funressnfv  47037  ffnafv  47165  tz6.12i-afv2  47237  iccpartiltu  47416  iccpartigtl  47417  icceuelpartlem  47429  fargshiftfo  47436  ichnreuop  47466  reupr  47516  bgoldbtbndlem2  47800  isubgredg  47859  upgrimtrlslem2  47898  cycl3grtrilem  47938  uspgrlimlem1  47980  gpgedg2ov  48050  gpgedg2iv  48051  rngcinvALTV  48257  srhmsubcALTV  48306  nnolog2flm1  48572  prelrrx2b  48696  rrxlinec  48718  eenglngeehlnm  48721