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  2440  nelneq  2860  nelneq2  2861  r19.35  3095  nssne1  3984  nssne2  3985  psssstr  4049  prproe  4848  iununi  5041  disjiun  5073  nbrne1  5104  nbrne2  5105  propeqop  5461  mosubopt  5464  relsnb  5758  relcnvtrg  6231  reuop  6257  dfpo2  6260  tz7.7  6349  suctr  6411  tz6.12i  6866  ssimaex  6925  chfnrn  7001  fvn0ssdmfun  7026  ffnfv  7071  f1elima  7218  elovmpt3rab1  7627  limsssuc  7801  nnsuc  7835  peano5  7844  dftpos4  8195  odi  8514  pssnn  9103  fineqvlem  9176  ordunifi  9200  wdom2d  9495  r1pwss  9708  alephval3  10032  infdif  10130  cff1  10180  cofsmo  10191  axdc3lem2  10373  zorn2lem6  10423  cfpwsdom  10507  prub  10917  prnmadd  10920  1re  11144  letr  11240  dedekindle  11310  addrid  11326  negf1o  11580  negfi  12105  xrletr  13109  0fz1  13498  elfzmlbp  13593  leisorel  14422  elss2prb  14450  exprelprel  14452  fi1uzind  14469  swrdnd  14617  sqrmo  15213  isprm2  16651  nprmdvds1  16676  oddprmdvds  16874  catsubcat  17806  funcestrcsetclem8  18113  funcestrcsetclem9  18114  fthestrcsetc  18116  fullestrcsetc  18117  funcsetcestrclem9  18129  fthsetcestrc  18131  fullsetcestrc  18132  pltletr  18307  mgmpropd  18619  issstrmgm  18621  mgm2nsgrplem3  18891  sgrp2nmndlem3  18896  fvcosymgeq  19404  sylow2alem2  19593  rngcinv  20614  srhmsubc  20657  islss  20929  gzrngunitlem  21412  pjdm2  21691  assamulgscmlem2  21880  gsumply1subr  22197  dmatmul  22462  decpmatmullem  22736  monmat2matmon  22789  chpscmat  22807  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  isclo2  23053  fbasfip  23833  ufileu  23884  alexsubALTlem2  24013  cnextcn  24032  metustbl  24531  cutbdaybnd2lim  27789  addsprop  27968  elntg2  29054  ushgredgedg  29298  ushgredgedgloop  29300  edgnbusgreu  29436  nb3grprlem1  29449  cusgrfilem1  29524  cusgrfilem2  29525  umgr2v2evtxel  29591  wlkcompim  29700  usgr2pth  29832  usgr2trlncrct  29874  wwlknp  29911  wlkiswwlks2lem3  29939  wlkiswwlksupgr2  29945  wlklnwwlkln2lem  29950  wwlksnext  29961  2pthdlem1  29998  umgr2adedgwlkonALT  30015  umgr2wlkon  30018  elwspths2spth  30038  rusgr0edg  30044  clwlkclwwlklem2a1  30062  clwlkclwwlklem2a  30068  clwwisshclwwslem  30084  loopclwwlkn1b  30112  clwwlkel  30116  clwwlkext2edg  30126  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  clwwlknonwwlknonb  30176  uhgr3cyclexlem  30251  upgr4cycl4dv4e  30255  eupth2lem3lem4  30301  frgruhgr0v  30334  numclwwlk1lem2f1  30427  numclwlk2lem2f  30447  numclwlk2lem2f1o  30449  frgrogt3nreg  30467  5oalem6  31730  eigorthi  31908  adjbd1o  32156  dmdbr7ati  32495  ssdifidlprm  33518  fmla1  35569  satffunlem2lem2  35588  fundmpss  35949  funbreq  35952  idinside  36266  tr0elw  36666  tr0el  36667  dfttc4  36712  bj-opelidres  37475  bj-eldiag2  37491  bj-fvimacnv0  37600  wl-eujustlem1  37913  poimirlem32  37973  sdclem2  38063  fdc1  38067  ismgmOLD  38171  lsatcvatlem  39495  atnle  39763  cvratlem  39867  ispsubcl2N  40393  trlord  41015  diaelrnN  41491  cdlemm10N  41564  dochexmidlem7  41912  fsuppind  43023  3impexpbicom  44907  sbcim2g  44965  suctrALT2VD  45262  suctrALT2  45263  3impexpVD  45282  3impexpbicomVD  45283  sbcim2gVD  45301  csbeq2gVD  45318  csbsngVD  45319  ax6e2ndeqVD  45335  2sb5ndVD  45336  infxrunb3rnmpt  45856  lptioo2  46061  lptioo1  46062  funressnfv  47491  ffnafv  47619  tz6.12i-afv2  47691  iccpartiltu  47882  iccpartigtl  47883  icceuelpartlem  47895  fargshiftfo  47902  ichnreuop  47932  reupr  47982  bgoldbtbndlem2  48282  isubgredg  48342  upgrimtrlslem2  48381  cycl3grtrilem  48422  uspgrlimlem1  48464  grlimprclnbgrvtx  48475  gpgedg2ov  48542  gpgedg2iv  48543  rngcinvALTV  48752  srhmsubcALTV  48801  nnolog2flm1  49066  prelrrx2b  49190  rrxlinec  49212  eenglngeehlnm  49215