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  2434  nelneq  2852  nelneq2  2853  r19.35  3087  nssne1  3998  nssne2  3999  psssstr  4060  prproe  4856  iununi  5048  disjiun  5080  nbrne1  5111  nbrne2  5112  propeqop  5450  mosubopt  5453  relsnb  5745  relcnvtrg  6215  reuop  6241  dfpo2  6244  tz7.7  6333  suctr  6395  tz6.12i  6848  ssimaex  6908  chfnrn  6983  fvn0ssdmfun  7008  ffnfv  7053  f1elima  7200  elovmpt3rab1  7609  limsssuc  7783  nnsuc  7817  peano5  7826  dftpos4  8178  odi  8497  pssnn  9082  fineqvlem  9155  ordunifi  9179  wdom2d  9472  r1pwss  9680  alephval3  10004  infdif  10102  cff1  10152  cofsmo  10163  axdc3lem2  10345  zorn2lem6  10395  cfpwsdom  10478  prub  10888  prnmadd  10891  1re  11115  letr  11210  dedekindle  11280  addrid  11296  negf1o  11550  negfi  12074  xrletr  13060  0fz1  13447  elfzmlbp  13542  leisorel  14367  elss2prb  14395  exprelprel  14397  fi1uzind  14414  swrdnd  14561  sqrmo  15158  isprm2  16593  nprmdvds1  16617  oddprmdvds  16815  catsubcat  17746  funcestrcsetclem8  18053  funcestrcsetclem9  18054  fthestrcsetc  18056  fullestrcsetc  18057  funcsetcestrclem9  18069  fthsetcestrc  18071  fullsetcestrc  18072  pltletr  18247  mgmpropd  18525  issstrmgm  18527  mgm2nsgrplem3  18794  sgrp2nmndlem3  18799  fvcosymgeq  19308  sylow2alem2  19497  rngcinv  20522  srhmsubc  20565  islss  20837  gzrngunitlem  21339  pjdm2  21618  assamulgscmlem2  21807  gsumply1subr  22116  dmatmul  22382  decpmatmullem  22656  monmat2matmon  22709  chpscmat  22727  chfacfscmulgsum  22745  chfacfpmmulgsum  22749  isclo2  22973  fbasfip  23753  ufileu  23804  alexsubALTlem2  23933  cnextcn  23952  metustbl  24452  scutbdaybnd2lim  27728  addsprop  27888  elntg2  28930  ushgredgedg  29174  ushgredgedgloop  29176  edgnbusgreu  29312  nb3grprlem1  29325  cusgrfilem1  29401  cusgrfilem2  29402  umgr2v2evtxel  29468  wlkcompim  29577  usgr2pth  29709  usgr2trlncrct  29751  wwlknp  29788  wlkiswwlks2lem3  29816  wlkiswwlksupgr2  29822  wlklnwwlkln2lem  29827  wwlksnext  29838  2pthdlem1  29875  umgr2adedgwlkonALT  29892  umgr2wlkon  29895  elwspths2spth  29912  rusgr0edg  29918  clwlkclwwlklem2a1  29936  clwlkclwwlklem2a  29942  clwwisshclwwslem  29958  loopclwwlkn1b  29986  clwwlkel  29990  clwwlkext2edg  30000  hashecclwwlkn1  30021  umgrhashecclwwlk  30022  clwwlknonwwlknonb  30050  uhgr3cyclexlem  30125  upgr4cycl4dv4e  30129  eupth2lem3lem4  30175  frgruhgr0v  30208  numclwwlk1lem2f1  30301  numclwlk2lem2f  30321  numclwlk2lem2f1o  30323  frgrogt3nreg  30341  5oalem6  31603  eigorthi  31781  adjbd1o  32029  dmdbr7ati  32368  ssdifidlprm  33395  fmla1  35364  satffunlem2lem2  35383  fundmpss  35744  funbreq  35747  idinside  36062  bj-opelidres  37139  bj-eldiag2  37155  bj-fvimacnv0  37264  poimirlem32  37636  sdclem2  37726  fdc1  37730  ismgmOLD  37834  lsatcvatlem  39032  atnle  39300  cvratlem  39404  ispsubcl2N  39930  trlord  40552  diaelrnN  41028  cdlemm10N  41101  dochexmidlem7  41449  fsuppind  42567  3impexpbicom  44458  sbcim2g  44516  suctrALT2VD  44813  suctrALT2  44814  3impexpVD  44833  3impexpbicomVD  44834  sbcim2gVD  44852  csbeq2gVD  44869  csbsngVD  44870  ax6e2ndeqVD  44886  2sb5ndVD  44887  infxrunb3rnmpt  45411  lptioo2  45616  lptioo1  45617  funressnfv  47031  ffnafv  47159  tz6.12i-afv2  47231  iccpartiltu  47410  iccpartigtl  47411  icceuelpartlem  47423  fargshiftfo  47430  ichnreuop  47460  reupr  47510  bgoldbtbndlem2  47794  isubgredg  47854  upgrimtrlslem2  47893  cycl3grtrilem  47934  uspgrlimlem1  47976  grlimprclnbgrvtx  47987  gpgedg2ov  48054  gpgedg2iv  48055  rngcinvALTV  48264  srhmsubcALTV  48313  nnolog2flm1  48579  prelrrx2b  48703  rrxlinec  48725  eenglngeehlnm  48728