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  2441  nelneq  2861  nelneq2  2862  r19.35  3096  nssne1  3998  nssne2  3999  psssstr  4063  prproe  4863  iununi  5056  disjiun  5088  nbrne1  5119  nbrne2  5120  propeqop  5463  mosubopt  5466  relsnb  5759  relcnvtrg  6233  reuop  6259  dfpo2  6262  tz7.7  6351  suctr  6413  tz6.12i  6868  ssimaex  6927  chfnrn  7003  fvn0ssdmfun  7028  ffnfv  7073  f1elima  7219  elovmpt3rab1  7628  limsssuc  7802  nnsuc  7836  peano5  7845  dftpos4  8197  odi  8516  pssnn  9105  fineqvlem  9178  ordunifi  9202  wdom2d  9497  r1pwss  9708  alephval3  10032  infdif  10130  cff1  10180  cofsmo  10191  axdc3lem2  10373  zorn2lem6  10423  cfpwsdom  10507  prub  10917  prnmadd  10920  1re  11144  letr  11239  dedekindle  11309  addrid  11325  negf1o  11579  negfi  12103  xrletr  13084  0fz1  13472  elfzmlbp  13567  leisorel  14395  elss2prb  14423  exprelprel  14425  fi1uzind  14442  swrdnd  14590  sqrmo  15186  isprm2  16621  nprmdvds1  16645  oddprmdvds  16843  catsubcat  17775  funcestrcsetclem8  18082  funcestrcsetclem9  18083  fthestrcsetc  18085  fullestrcsetc  18086  funcsetcestrclem9  18098  fthsetcestrc  18100  fullsetcestrc  18101  pltletr  18276  mgmpropd  18588  issstrmgm  18590  mgm2nsgrplem3  18857  sgrp2nmndlem3  18862  fvcosymgeq  19370  sylow2alem2  19559  rngcinv  20582  srhmsubc  20625  islss  20897  gzrngunitlem  21399  pjdm2  21678  assamulgscmlem2  21868  gsumply1subr  22186  dmatmul  22453  decpmatmullem  22727  monmat2matmon  22780  chpscmat  22798  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  isclo2  23044  fbasfip  23824  ufileu  23875  alexsubALTlem2  24004  cnextcn  24023  metustbl  24522  cutbdaybnd2lim  27805  addsprop  27984  elntg2  29070  ushgredgedg  29314  ushgredgedgloop  29316  edgnbusgreu  29452  nb3grprlem1  29465  cusgrfilem1  29541  cusgrfilem2  29542  umgr2v2evtxel  29608  wlkcompim  29717  usgr2pth  29849  usgr2trlncrct  29891  wwlknp  29928  wlkiswwlks2lem3  29956  wlkiswwlksupgr2  29962  wlklnwwlkln2lem  29967  wwlksnext  29978  2pthdlem1  30015  umgr2adedgwlkonALT  30032  umgr2wlkon  30035  elwspths2spth  30055  rusgr0edg  30061  clwlkclwwlklem2a1  30079  clwlkclwwlklem2a  30085  clwwisshclwwslem  30101  loopclwwlkn1b  30129  clwwlkel  30133  clwwlkext2edg  30143  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  clwwlknonwwlknonb  30193  uhgr3cyclexlem  30268  upgr4cycl4dv4e  30272  eupth2lem3lem4  30318  frgruhgr0v  30351  numclwwlk1lem2f1  30444  numclwlk2lem2f  30464  numclwlk2lem2f1o  30466  frgrogt3nreg  30484  5oalem6  31747  eigorthi  31925  adjbd1o  32173  dmdbr7ati  32512  ssdifidlprm  33551  fmla1  35603  satffunlem2lem2  35622  fundmpss  35983  funbreq  35986  idinside  36300  bj-opelidres  37416  bj-eldiag2  37432  bj-fvimacnv0  37541  wl-eujustlem1  37843  poimirlem32  37903  sdclem2  37993  fdc1  37997  ismgmOLD  38101  lsatcvatlem  39425  atnle  39693  cvratlem  39797  ispsubcl2N  40323  trlord  40945  diaelrnN  41421  cdlemm10N  41494  dochexmidlem7  41842  fsuppind  42948  3impexpbicom  44836  sbcim2g  44894  suctrALT2VD  45191  suctrALT2  45192  3impexpVD  45211  3impexpbicomVD  45212  sbcim2gVD  45230  csbeq2gVD  45247  csbsngVD  45248  ax6e2ndeqVD  45264  2sb5ndVD  45265  infxrunb3rnmpt  45786  lptioo2  45991  lptioo1  45992  funressnfv  47403  ffnafv  47531  tz6.12i-afv2  47603  iccpartiltu  47782  iccpartigtl  47783  icceuelpartlem  47795  fargshiftfo  47802  ichnreuop  47832  reupr  47882  bgoldbtbndlem2  48166  isubgredg  48226  upgrimtrlslem2  48265  cycl3grtrilem  48306  uspgrlimlem1  48348  grlimprclnbgrvtx  48359  gpgedg2ov  48426  gpgedg2iv  48427  rngcinvALTV  48636  srhmsubcALTV  48685  nnolog2flm1  48950  prelrrx2b  49074  rrxlinec  49096  eenglngeehlnm  49099