Theorem biimpcd 250

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  biimpac  479  axc16i  2444  nelneq  2863  nelneq2  2864  r19.35  3097  nssne1  3977  nssne2  3978  psssstr  4040  prproe  4836  iununi  5028  disjiun  5060  nbrne1  5091  nbrne2  5092  propeqop  5448  mosubopt  5451  relsnb  5745  relcnvtrg  6218  reuop  6244  dfpo2  6247  tz7.7  6336  suctr  6398  tz6.12i  6853  ssimaex  6912  chfnrn  6990  fvn0ssdmfun  7015  ffnfv  7060  f1elima  7207  elovmpt3rab1  7616  limsssuc  7790  nnsuc  7824  peano5  7833  dftpos4  8185  odi  8504  pssnn  9093  fineqvlem  9166  ordunifi  9190  wdom2d  9485  r1pwss  9699  alephval3  10023  infdif  10121  cff1  10171  cofsmo  10182  axdc3lem2  10364  zorn2lem6  10414  cfpwsdom  10498  prub  10908  prnmadd  10911  1re  11135  letr  11231  dedekindle  11301  addrid  11317  negf1o  11571  negfi  12096  xrletr  13100  0fz1  13489  elfzmlbp  13584  leisorel  14413  elss2prb  14441  exprelprel  14443  fi1uzind  14460  swrdnd  14608  sqrmo  15204  isprm2  16642  nprmdvds1  16667  oddprmdvds  16865  catsubcat  17797  funcestrcsetclem8  18104  funcestrcsetclem9  18105  fthestrcsetc  18107  fullestrcsetc  18108  funcsetcestrclem9  18120  fthsetcestrc  18122  fullsetcestrc  18123  pltletr  18298  mgmpropd  18610  issstrmgm  18612  mgm2nsgrplem3  18882  sgrp2nmndlem3  18887  fvcosymgeq  19395  sylow2alem2  19584  rngcinv  20609  srhmsubc  20652  islss  20924  gzrngunitlem  21407  pjdm2  21686  assamulgscmlem2  21875  gsumply1subr  22218  dmatmul  22480  decpmatmullem  22754  monmat2matmon  22807  chpscmat  22825  chfacfscmulgsum  22843  chfacfpmmulgsum  22847  isclo2  23071  fbasfip  23851  ufileu  23902  alexsubALTlem2  24031  cnextcn  24050  metustbl  24549  cutbdaybnd2lim  27807  addsprop  27986  elntg2  29072  ushgredgedg  29316  ushgredgedgloop  29318  edgnbusgreu  29454  nb3grprlem1  29467  cusgrfilem1  29542  cusgrfilem2  29543  umgr2v2evtxel  29609  wlkcompim  29718  usgr2pth  29850  usgr2trlncrct  29892  wwlknp  29929  wlkiswwlks2lem3  29957  wlkiswwlksupgr2  29963  wlklnwwlkln2lem  29968  wwlksnext  29979  2pthdlem1  30016  umgr2adedgwlkonALT  30033  umgr2wlkon  30036  elwspths2spth  30056  rusgr0edg  30062  clwlkclwwlklem2a1  30080  clwlkclwwlklem2a  30086  clwwisshclwwslem  30102  loopclwwlkn1b  30130  clwwlkel  30134  clwwlkext2edg  30144  hashecclwwlkn1  30165  umgrhashecclwwlk  30166  clwwlknonwwlknonb  30194  uhgr3cyclexlem  30269  upgr4cycl4dv4e  30273  eupth2lem3lem4  30319  frgruhgr0v  30352  numclwwlk1lem2f1  30445  numclwlk2lem2f  30465  numclwlk2lem2f1o  30467  frgrogt3nreg  30485  5oalem6  31748  eigorthi  31926  adjbd1o  32174  dmdbr7ati  32513  ssdifidlprm  33541  fmla1  35615  satffunlem2lem2  35634  fundmpss  35995  funbreq  35998  idinside  36312  tr0elw  36712  tr0el  36713  dfttc4  36758  bj-opelidres  37521  bj-eldiag2  37537  bj-fvimacnv0  37646  wl-eujustlem1  37959  poimirlem32  38019  sdclem2  38109  fdc1  38113  ismgmOLD  38217  lsatcvatlem  39541  atnle  39809  cvratlem  39913  ispsubcl2N  40439  trlord  41061  diaelrnN  41537  cdlemm10N  41610  dochexmidlem7  41958  fsuppind  43040  3impexpbicom  44924  sbcim2g  44982  suctrALT2VD  45279  suctrALT2  45280  3impexpVD  45299  3impexpbicomVD  45300  sbcim2gVD  45318  csbeq2gVD  45335  csbsngVD  45336  ax6e2ndeqVD  45352  2sb5ndVD  45353  infxrunb3rnmpt  45871  lptioo2  46076  lptioo1  46077  funressnfv  47506  ffnafv  47634  tz6.12i-afv2  47706  iccpartiltu  47897  iccpartigtl  47898  icceuelpartlem  47910  fargshiftfo  47917  ichnreuop  47947  reupr  47997  bgoldbtbndlem2  48297  isubgredg  48357  upgrimtrlslem2  48396  cycl3grtrilem  48437  uspgrlimlem1  48479  grlimprclnbgrvtx  48490  gpgedg2ov  48557  gpgedg2iv  48558  rngcinvALTV  48767  srhmsubcALTV  48816  nnolog2flm1  49081  prelrrx2b  49205  rrxlinec  49227  eenglngeehlnm  49230