Theorem biimpcd 251

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  biimpac  481  axc16i  2461  nelneq  2880  nelneq2  2881  r19.35  3114  nssne1  3993  nssne2  3994  psssstr  4058  prproe  4857  iununi  5050  disjiun  5082  nbrne1  5113  nbrne2  5114  propeqop  5470  mosubopt  5473  relsnb  5768  relcnvtrg  6243  reuop  6269  dfpo2  6272  tz7.7  6361  suctr  6423  tz6.12i  6882  ssimaex  6941  chfnrn  7019  fvn0ssdmfun  7044  ffnfv  7089  f1elima  7236  elovmpt3rab1  7645  limsssuc  7819  nnsuc  7853  peano5  7863  dftpos4  8213  odi  8536  pssnn  9126  fineqvlem  9199  ordunifi  9223  wdom2d  9518  r1pwss  9732  alephval3  10056  infdif  10154  cff1  10205  cofsmo  10216  axdc3lem2  10398  zorn2lem6  10448  cfpwsdom  10532  prub  10942  prnmadd  10945  1re  11171  letr  11267  dedekindle  11337  addrid  11353  negf1o  11607  negfi  12131  xrletr  13150  0fz1  13539  elfzmlbp  13634  leisorel  14463  elss2prb  14491  exprelprel  14493  fi1uzind  14510  swrdnd  14658  sqrmo  15254  isprm2  16692  nprmdvds1  16717  oddprmdvds  16915  catsubcat  17848  funcestrcsetclem8  18155  funcestrcsetclem9  18156  fthestrcsetc  18158  fullestrcsetc  18159  funcsetcestrclem9  18171  fthsetcestrc  18173  fullsetcestrc  18174  pltletr  18349  mgmpropd  18661  issstrmgm  18663  mgm2nsgrplem3  18933  sgrp2nmndlem3  18938  fvcosymgeq  19445  sylow2alem2  19634  rngcinv  20659  srhmsubc  20702  islss  20974  gzrngunitlem  21457  pjdm2  21736  assamulgscmlem2  21925  gsumply1subr  22268  dmatmul  22530  decpmatmullem  22804  monmat2matmon  22857  chpscmat  22875  chfacfscmulgsum  22893  chfacfpmmulgsum  22897  isclo2  23121  fbasfip  23901  ufileu  23952  alexsubALTlem2  24081  cnextcn  24100  metustbl  24599  cutbdaybnd2lim  27860  addsprop  28039  elntg2  29125  ushgredgedg  29369  ushgredgedgloop  29371  edgnbusgreu  29507  nb3grprlem1  29520  cusgrfilem1  29595  cusgrfilem2  29596  umgr2v2evtxel  29662  wlkcompim  29771  usgr2pth  29903  usgr2trlncrct  29945  wwlknp  29982  wlkiswwlks2lem3  30010  wlkiswwlksupgr2  30016  wlklnwwlkln2lem  30021  wwlksnext  30032  2pthdlem1  30069  umgr2adedgwlkonALT  30086  umgr2wlkon  30089  elwspths2spth  30109  rusgr0edg  30115  clwlkclwwlklem2a1  30133  clwlkclwwlklem2a  30139  clwwisshclwwslem  30155  loopclwwlkn1b  30183  clwwlkel  30187  clwwlkext2edg  30197  hashecclwwlkn1  30218  umgrhashecclwwlk  30219  clwwlknonwwlknonb  30247  uhgr3cyclexlem  30322  upgr4cycl4dv4e  30326  eupth2lem3lem4  30372  frgruhgr0v  30405  numclwwlk1lem2f1  30498  numclwlk2lem2f  30518  numclwlk2lem2f1o  30520  frgrogt3nreg  30538  5oalem6  31801  eigorthi  31979  adjbd1o  32227  dmdbr7ati  32566  ssdifidlprm  33599  fmla1  35685  satffunlem2lem2  35704  fundmpss  36065  funbreq  36068  idinside  36382  tr0elw  36792  tr0el  36793  dfttc4  36838  bj-opelidres  37601  bj-eldiag2  37617  bj-fvimacnv0  37726  wl-eujustlem1  38039  poimirlem32  38099  sdclem2  38189  fdc1  38193  ismgmOLD  38297  lsatcvatlem  39621  atnle  39889  cvratlem  39993  ispsubcl2N  40519  trlord  41141  diaelrnN  41617  cdlemm10N  41690  dochexmidlem7  42038  fsuppind  43120  3impexpbicom  45004  sbcim2g  45062  suctrALT2VD  45359  suctrALT2  45360  3impexpVD  45379  3impexpbicomVD  45380  sbcim2gVD  45398  csbeq2gVD  45415  csbsngVD  45416  ax6e2ndeqVD  45432  2sb5ndVD  45433  infxrunb3rnmpt  45950  lptioo2  46155  lptioo1  46156  funressnfv  47585  ffnafv  47713  tz6.12i-afv2  47785  iccpartiltu  47976  iccpartigtl  47977  icceuelpartlem  47989  fargshiftfo  47996  ichnreuop  48026  reupr  48076  bgoldbtbndlem2  48376  isubgredg  48436  upgrimtrlslem2  48475  cycl3grtrilem  48516  uspgrlimlem1  48558  grlimprclnbgrvtx  48569  gpgedg2ov  48636  gpgedg2iv  48637  rngcinvALTV  48846  srhmsubcALTV  48895  nnolog2flm1  49160  prelrrx2b  49284  rrxlinec  49306  eenglngeehlnm  49309