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  2439  nelneq  2863  nelneq2  2864  r19.35  3106  nssne1  4058  nssne2  4059  psssstr  4119  prproe  4910  iununi  5104  disjiun  5136  nbrne1  5167  nbrne2  5168  propeqop  5517  mosubopt  5520  relsnb  5815  relcnvtrg  6288  reuop  6315  dfpo2  6318  tz7.7  6412  suctr  6472  tz6.12i  6935  ssimaex  6994  chfnrn  7069  fvn0ssdmfun  7094  ffnfv  7139  f1elima  7283  elovmpt3rab1  7693  limsssuc  7871  nnsuc  7905  peano5  7916  dftpos4  8269  odi  8616  pssnn  9207  fineqvlem  9296  ordunifi  9324  wdom2d  9618  r1pwss  9822  alephval3  10148  infdif  10246  cff1  10296  cofsmo  10307  axdc3lem2  10489  zorn2lem6  10539  cfpwsdom  10622  prub  11032  prnmadd  11035  1re  11259  letr  11353  dedekindle  11423  addrid  11439  negf1o  11691  negfi  12215  xrletr  13197  0fz1  13581  elfzmlbp  13676  leisorel  14496  elss2prb  14524  exprelprel  14526  fi1uzind  14543  swrdnd  14689  sqrmo  15287  isprm2  16716  nprmdvds1  16740  oddprmdvds  16937  catsubcat  17890  funcestrcsetclem8  18203  funcestrcsetclem9  18204  fthestrcsetc  18206  fullestrcsetc  18207  funcsetcestrclem9  18219  fthsetcestrc  18221  fullsetcestrc  18222  pltletr  18401  mgmpropd  18677  issstrmgm  18679  mgm2nsgrplem3  18946  sgrp2nmndlem3  18951  fvcosymgeq  19462  sylow2alem2  19651  rngcinv  20654  srhmsubc  20697  islss  20950  gzrngunitlem  21468  pjdm2  21749  assamulgscmlem2  21938  gsumply1subr  22251  dmatmul  22519  decpmatmullem  22793  monmat2matmon  22846  chpscmat  22864  chfacfscmulgsum  22882  chfacfpmmulgsum  22886  isclo2  23112  fbasfip  23892  ufileu  23943  alexsubALTlem2  24072  cnextcn  24091  metustbl  24595  scutbdaybnd2lim  27877  addsprop  28024  elntg2  29015  ushgredgedg  29261  ushgredgedgloop  29263  edgnbusgreu  29399  nb3grprlem1  29412  cusgrfilem1  29488  cusgrfilem2  29489  umgr2v2evtxel  29555  wlkcompim  29665  usgr2pth  29797  usgr2trlncrct  29836  wwlknp  29873  wlkiswwlks2lem3  29901  wlkiswwlksupgr2  29907  wlklnwwlkln2lem  29912  wwlksnext  29923  2pthdlem1  29960  umgr2adedgwlkonALT  29977  umgr2wlkon  29980  elwspths2spth  29997  rusgr0edg  30003  clwlkclwwlklem2a1  30021  clwlkclwwlklem2a  30027  clwwisshclwwslem  30043  loopclwwlkn1b  30071  clwwlkel  30075  clwwlkext2edg  30085  hashecclwwlkn1  30106  umgrhashecclwwlk  30107  clwwlknonwwlknonb  30135  uhgr3cyclexlem  30210  upgr4cycl4dv4e  30214  eupth2lem3lem4  30260  frgruhgr0v  30293  numclwwlk1lem2f1  30386  numclwlk2lem2f  30406  numclwlk2lem2f1o  30408  frgrogt3nreg  30426  5oalem6  31688  eigorthi  31866  adjbd1o  32114  dmdbr7ati  32453  ssdifidlprm  33466  fmla1  35372  satffunlem2lem2  35391  fundmpss  35748  funbreq  35751  idinside  36066  bj-opelidres  37144  bj-eldiag2  37160  bj-fvimacnv0  37269  poimirlem32  37639  sdclem2  37729  fdc1  37733  ismgmOLD  37837  lsatcvatlem  39031  atnle  39299  cvratlem  39404  ispsubcl2N  39930  trlord  40552  diaelrnN  41028  cdlemm10N  41101  dochexmidlem7  41449  fsuppind  42577  3impexpbicom  44477  sbcim2g  44536  suctrALT2VD  44834  suctrALT2  44835  3impexpVD  44854  3impexpbicomVD  44855  sbcim2gVD  44873  csbeq2gVD  44890  csbsngVD  44891  ax6e2ndeqVD  44907  2sb5ndVD  44908  infxrunb3rnmpt  45378  lptioo2  45587  lptioo1  45588  funressnfv  46993  ffnafv  47121  tz6.12i-afv2  47193  iccpartiltu  47347  iccpartigtl  47348  icceuelpartlem  47360  fargshiftfo  47367  ichnreuop  47397  reupr  47447  bgoldbtbndlem2  47731  isubgredg  47790  uspgrlimlem1  47891  rngcinvALTV  48120  srhmsubcALTV  48169  nnolog2flm1  48440  prelrrx2b  48564  rrxlinec  48586  eenglngeehlnm  48589