Theorem biimpd 143

Description: Deduce an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
biimpd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimpd	⊢ (𝜑 → (𝜓 → 𝜒))

Proof of Theorem biimpd

Step	Hyp	Ref	Expression
1		biimpd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		biimp 117	. 2 ⊢ ((𝜓 ↔ 𝜒) → (𝜓 → 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbid  146  sylibd  148  sylbid  149  mpbidi  150  syl5ib  153  syl6bi  162  ibi  175  imbi1d  230  biimpa  294  mtbird  663  mtbiri  665  orbi2d  780  pm5.15dc  1371  exlimd2  1575  exintr  1614  19.9d  1641  19.23t  1657  chvarfv  1680  dral1  1710  spimt  1716  cbvalv1  1731  cbvalh  1733  chvar  1737  exdistrfor  1780  sbequi  1819  spv  1840  cbvexvw  1900  eqrdav  2156  cleqh  2257  ceqsalg  2740  vtoclf  2765  vtocl2  2767  vtocl3  2768  spcdv  2797  rspcdv  2819  elabgt  2853  sbcn1  2984  sbcim1  2985  sbcbi1  2986  sbeqalb  2993  sbcel21v  3001  eqrd  3146  exmidsssn  4164  exmidsssnc  4165  copsexg  4205  euotd  4215  rexxfrd  4424  relop  4737  elres  4903  rnxpid  5021  relcnvtr  5106  iotaval  5147  mpteqb  5559  elfvmptrab  5564  chfnrn  5579  elpreima  5587  ffnfv  5626  f1elima  5724  f1eqcocnv  5742  fliftfun  5747  isoresbr  5760  isotr  5767  ovmpodv2  5955  smoiso  6250  nnaordi  6456  nnaword  6459  nnawordi  6463  xpider  6552  iinerm  6553  mptelixpg  6680  dom2lem  6718  nneneq  6803  exmidpw  6854  f1dmvrnfibi  6889  ismkvnex  7099  pr2nelem  7127  exmidfodomrlemeldju  7135  exmidfodomrlemreseldju  7136  addcanpig  7255  mulcanpig  7256  enqer  7279  ltexnqi  7330  prarloclemlo  7415  genpcdl  7440  genpcuu  7441  appdivnq  7484  ltprordil  7510  1idprl  7511  1idpru  7512  ltexprlemm  7521  ltexprlemopu  7524  ltexprlemru  7533  cauappcvgprlemladdru  7577  cauappcvgprlemladdrl  7578  caucvgprprlemopu  7620  caucvgsrlemoffcau  7719  caucvgsrlemoffres  7721  ltrenn  7776  axpre-ltadd  7807  addn0nid  8250  apne  8499  prodgt02  8725  prodge02  8727  mulgt1  8735  divgt0  8744  divge0  8745  cju  8833  nnsub  8873  nominpos  9071  zltnle  9214  nn0n0n1ge2  9235  zdcle  9241  btwnnz  9259  uzm1  9470  supinfneg  9507  infsupneg  9508  ublbneg  9523  cnref1o  9560  ltsubrp  9598  ltaddrp  9599  npnflt  9720  nmnfgt  9723  ge0nemnf  9729  xltnegi  9740  xnn0xadd0  9772  iccsupr  9871  icoshft  9895  iccshftri  9900  iccshftli  9902  iccdili  9904  icccntri  9906  fzdcel  9943  fznlem  9944  fzen  9946  fzofzim  10091  eluzgtdifelfzo  10100  elfzonelfzo  10133  qltnle  10149  addmodlteq  10301  apexp1  10596  fihashf1rn  10667  cjre  10786  caucvgre  10885  icodiamlt  11084  zsumdc  11285  zproddc  11480  reeff1  11601  dvdsmod0  11693  dvds2lem  11703  muldvds1  11716  dvdscmulr  11720  dvdsmulcr  11721  dvdsdivcl  11746  oddnn02np1  11775  ndvdsadd  11826  zeqzmulgcd  11858  bezoutlemmain  11886  dfgcd2  11902  gcdmultiple  11908  coprmdvds  11973  divgcdodd  12022  isprm6  12026  prmdvdsexpr  12029  cncongrprm  12036  phiprmpw  12101  modprm0  12133  pythagtriplem4  12147  lmss  12688  cnplimcim  13078  dvcn  13106  ch2var  13383  bj-rspgt  13402  bj-charfundcALT  13426  bj-nntrans  13568  bj-nnelirr  13570  bj-omtrans  13573  setindft  13582  bj-inf2vnlem3  13589  bj-inf2vnlem4  13590  bj-findis  13596  pw1nct  13617