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  3985  nssne2  3986  psssstr  4050  prproe  4849  iununi  5042  disjiun  5074  nbrne1  5105  nbrne2  5106  propeqop  5456  mosubopt  5459  relsnb  5752  relcnvtrg  6226  reuop  6252  dfpo2  6255  tz7.7  6344  suctr  6406  tz6.12i  6861  ssimaex  6920  chfnrn  6996  fvn0ssdmfun  7021  ffnfv  7066  f1elima  7212  elovmpt3rab1  7621  limsssuc  7795  nnsuc  7829  peano5  7838  dftpos4  8189  odi  8508  pssnn  9097  fineqvlem  9170  ordunifi  9194  wdom2d  9489  r1pwss  9702  alephval3  10026  infdif  10124  cff1  10174  cofsmo  10185  axdc3lem2  10367  zorn2lem6  10417  cfpwsdom  10501  prub  10911  prnmadd  10914  1re  11138  letr  11234  dedekindle  11304  addrid  11320  negf1o  11574  negfi  12099  xrletr  13103  0fz1  13492  elfzmlbp  13587  leisorel  14416  elss2prb  14444  exprelprel  14446  fi1uzind  14463  swrdnd  14611  sqrmo  15207  isprm2  16645  nprmdvds1  16670  oddprmdvds  16868  catsubcat  17800  funcestrcsetclem8  18107  funcestrcsetclem9  18108  fthestrcsetc  18110  fullestrcsetc  18111  funcsetcestrclem9  18123  fthsetcestrc  18125  fullsetcestrc  18126  pltletr  18301  mgmpropd  18613  issstrmgm  18615  mgm2nsgrplem3  18885  sgrp2nmndlem3  18890  fvcosymgeq  19398  sylow2alem2  19587  rngcinv  20608  srhmsubc  20651  islss  20923  gzrngunitlem  21425  pjdm2  21704  assamulgscmlem2  21893  gsumply1subr  22210  dmatmul  22475  decpmatmullem  22749  monmat2matmon  22802  chpscmat  22820  chfacfscmulgsum  22838  chfacfpmmulgsum  22842  isclo2  23066  fbasfip  23846  ufileu  23897  alexsubALTlem2  24026  cnextcn  24045  metustbl  24544  cutbdaybnd2lim  27806  addsprop  27985  elntg2  29071  ushgredgedg  29315  ushgredgedgloop  29317  edgnbusgreu  29453  nb3grprlem1  29466  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  33536  fmla1  35588  satffunlem2lem2  35607  fundmpss  35968  funbreq  35971  idinside  36285  tr0elw  36685  tr0el  36686  dfttc4  36731  bj-opelidres  37494  bj-eldiag2  37510  bj-fvimacnv0  37619  wl-eujustlem1  37930  poimirlem32  37990  sdclem2  38080  fdc1  38084  ismgmOLD  38188  lsatcvatlem  39512  atnle  39780  cvratlem  39884  ispsubcl2N  40410  trlord  41032  diaelrnN  41508  cdlemm10N  41581  dochexmidlem7  41929  fsuppind  43040  3impexpbicom  44928  sbcim2g  44986  suctrALT2VD  45283  suctrALT2  45284  3impexpVD  45303  3impexpbicomVD  45304  sbcim2gVD  45322  csbeq2gVD  45339  csbsngVD  45340  ax6e2ndeqVD  45356  2sb5ndVD  45357  infxrunb3rnmpt  45877  lptioo2  46082  lptioo1  46083  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