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		bi1 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  662  mtbiri  664  orbi2d  779  pm5.15dc  1367  exlimd2  1574  exintr  1613  19.9d  1639  19.23t  1655  dral1  1708  spimt  1714  cbvalh  1726  chvar  1730  exdistrfor  1772  sbequi  1811  spv  1832  eqrdav  2138  cleqh  2239  ceqsalg  2714  vtoclf  2739  vtocl2  2741  vtocl3  2742  spcdv  2771  rspcdv  2792  elabgt  2825  sbcn1  2956  sbcim1  2957  sbcbi1  2958  sbeqalb  2965  sbcel21v  2973  eqrd  3115  exmidsssn  4125  exmidsssnc  4126  copsexg  4166  euotd  4176  rexxfrd  4384  relop  4689  elres  4855  rnxpid  4973  relcnvtr  5058  iotaval  5099  mpteqb  5511  elfvmptrab  5516  chfnrn  5531  elpreima  5539  ffnfv  5578  f1elima  5674  f1eqcocnv  5692  fliftfun  5697  isoresbr  5710  isotr  5717  ovmpodv2  5904  smoiso  6199  nnaordi  6404  nnaword  6407  nnawordi  6411  xpider  6500  iinerm  6501  mptelixpg  6628  dom2lem  6666  nneneq  6751  exmidpw  6802  f1dmvrnfibi  6832  ismkvnex  7029  pr2nelem  7047  exmidfodomrlemeldju  7055  exmidfodomrlemreseldju  7056  addcanpig  7142  mulcanpig  7143  enqer  7166  ltexnqi  7217  prarloclemlo  7302  genpcdl  7327  genpcuu  7328  appdivnq  7371  ltprordil  7397  1idprl  7398  1idpru  7399  ltexprlemm  7408  ltexprlemopu  7411  ltexprlemru  7420  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  caucvgprprlemopu  7507  caucvgsrlemoffcau  7606  caucvgsrlemoffres  7608  ltrenn  7663  axpre-ltadd  7694  addn0nid  8136  apne  8385  prodgt02  8611  prodge02  8613  mulgt1  8621  divgt0  8630  divge0  8631  cju  8719  nnsub  8759  nominpos  8957  zltnle  9100  nn0n0n1ge2  9121  zdcle  9127  btwnnz  9145  uzm1  9356  supinfneg  9390  infsupneg  9391  ublbneg  9405  cnref1o  9440  ltsubrp  9478  ltaddrp  9479  npnflt  9598  nmnfgt  9601  ge0nemnf  9607  xltnegi  9618  xnn0xadd0  9650  iccsupr  9749  icoshft  9773  iccshftri  9778  iccshftli  9780  iccdili  9782  icccntri  9784  fzdcel  9820  fznlem  9821  fzen  9823  fzofzim  9965  eluzgtdifelfzo  9974  elfzonelfzo  10007  qltnle  10023  addmodlteq  10171  fihashf1rn  10535  cjre  10654  caucvgre  10753  icodiamlt  10952  zsumdc  11153  reeff1  11407  dvds2lem  11505  muldvds1  11518  dvdscmulr  11522  dvdsmulcr  11523  dvdsdivcl  11548  oddnn02np1  11577  ndvdsadd  11628  zeqzmulgcd  11659  bezoutlemmain  11686  dfgcd2  11702  gcdmultiple  11708  coprmdvds  11773  divgcdodd  11821  isprm6  11825  prmdvdsexpr  11828  cncongrprm  11835  phiprmpw  11898  lmss  12415  cnplimcim  12805  dvcn  12833  ch2var  12974  bj-rspgt  12993  bj-nntrans  13149  bj-nnelirr  13151  bj-omtrans  13154  setindft  13163  bj-inf2vnlem3  13170  bj-inf2vnlem4  13171  bj-findis  13177