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  2438  nelneq  2858  nelneq2  2859  r19.35  3092  nssne1  3994  nssne2  3995  psssstr  4059  prproe  4859  iununi  5052  disjiun  5084  nbrne1  5115  nbrne2  5116  propeqop  5453  mosubopt  5456  relsnb  5749  relcnvtrg  6223  reuop  6249  dfpo2  6252  tz7.7  6341  suctr  6403  tz6.12i  6858  ssimaex  6917  chfnrn  6992  fvn0ssdmfun  7017  ffnfv  7062  f1elima  7207  elovmpt3rab1  7616  limsssuc  7790  nnsuc  7824  peano5  7833  dftpos4  8185  odi  8504  pssnn  9091  fineqvlem  9164  ordunifi  9188  wdom2d  9483  r1pwss  9694  alephval3  10018  infdif  10116  cff1  10166  cofsmo  10177  axdc3lem2  10359  zorn2lem6  10409  cfpwsdom  10493  prub  10903  prnmadd  10906  1re  11130  letr  11225  dedekindle  11295  addrid  11311  negf1o  11565  negfi  12089  xrletr  13070  0fz1  13458  elfzmlbp  13553  leisorel  14381  elss2prb  14409  exprelprel  14411  fi1uzind  14428  swrdnd  14576  sqrmo  15172  isprm2  16607  nprmdvds1  16631  oddprmdvds  16829  catsubcat  17761  funcestrcsetclem8  18068  funcestrcsetclem9  18069  fthestrcsetc  18071  fullestrcsetc  18072  funcsetcestrclem9  18084  fthsetcestrc  18086  fullsetcestrc  18087  pltletr  18262  mgmpropd  18574  issstrmgm  18576  mgm2nsgrplem3  18843  sgrp2nmndlem3  18848  fvcosymgeq  19356  sylow2alem2  19545  rngcinv  20568  srhmsubc  20611  islss  20883  gzrngunitlem  21385  pjdm2  21664  assamulgscmlem2  21854  gsumply1subr  22172  dmatmul  22439  decpmatmullem  22713  monmat2matmon  22766  chpscmat  22784  chfacfscmulgsum  22802  chfacfpmmulgsum  22806  isclo2  23030  fbasfip  23810  ufileu  23861  alexsubALTlem2  23990  cnextcn  24009  metustbl  24508  scutbdaybnd2lim  27785  addsprop  27946  elntg2  29007  ushgredgedg  29251  ushgredgedgloop  29253  edgnbusgreu  29389  nb3grprlem1  29402  cusgrfilem1  29478  cusgrfilem2  29479  umgr2v2evtxel  29545  wlkcompim  29654  usgr2pth  29786  usgr2trlncrct  29828  wwlknp  29865  wlkiswwlks2lem3  29893  wlkiswwlksupgr2  29899  wlklnwwlkln2lem  29904  wwlksnext  29915  2pthdlem1  29952  umgr2adedgwlkonALT  29969  umgr2wlkon  29972  elwspths2spth  29992  rusgr0edg  29998  clwlkclwwlklem2a1  30016  clwlkclwwlklem2a  30022  clwwisshclwwslem  30038  loopclwwlkn1b  30066  clwwlkel  30070  clwwlkext2edg  30080  hashecclwwlkn1  30101  umgrhashecclwwlk  30102  clwwlknonwwlknonb  30130  uhgr3cyclexlem  30205  upgr4cycl4dv4e  30209  eupth2lem3lem4  30255  frgruhgr0v  30288  numclwwlk1lem2f1  30381  numclwlk2lem2f  30401  numclwlk2lem2f1o  30403  frgrogt3nreg  30421  5oalem6  31683  eigorthi  31861  adjbd1o  32109  dmdbr7ati  32448  ssdifidlprm  33488  fmla1  35530  satffunlem2lem2  35549  fundmpss  35910  funbreq  35913  idinside  36227  bj-opelidres  37305  bj-eldiag2  37321  bj-fvimacnv0  37430  wl-eujustlem1  37732  poimirlem32  37792  sdclem2  37882  fdc1  37886  ismgmOLD  37990  lsatcvatlem  39248  atnle  39516  cvratlem  39620  ispsubcl2N  40146  trlord  40768  diaelrnN  41244  cdlemm10N  41317  dochexmidlem7  41665  fsuppind  42775  3impexpbicom  44663  sbcim2g  44721  suctrALT2VD  45018  suctrALT2  45019  3impexpVD  45038  3impexpbicomVD  45039  sbcim2gVD  45057  csbeq2gVD  45074  csbsngVD  45075  ax6e2ndeqVD  45091  2sb5ndVD  45092  infxrunb3rnmpt  45614  lptioo2  45819  lptioo1  45820  funressnfv  47231  ffnafv  47359  tz6.12i-afv2  47431  iccpartiltu  47610  iccpartigtl  47611  icceuelpartlem  47623  fargshiftfo  47630  ichnreuop  47660  reupr  47710  bgoldbtbndlem2  47994  isubgredg  48054  upgrimtrlslem2  48093  cycl3grtrilem  48134  uspgrlimlem1  48176  grlimprclnbgrvtx  48187  gpgedg2ov  48254  gpgedg2iv  48255  rngcinvALTV  48464  srhmsubcALTV  48513  nnolog2flm1  48778  prelrrx2b  48902  rrxlinec  48924  eenglngeehlnm  48927