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-1 5  ax-2 6  ax-mp 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  292  mtbird  645  mtbiri  647  orbi2d  762  pm5.15dc  1350  exlimd2  1557  exintr  1596  19.9d  1622  19.23t  1638  dral1  1691  spimt  1697  cbvalh  1709  chvar  1713  exdistrfor  1754  sbequi  1793  spv  1814  eqrdav  2114  cleqh  2214  ceqsalg  2685  vtoclf  2710  vtocl2  2712  vtocl3  2713  spcdv  2742  rspcdv  2763  elabgt  2795  sbcn1  2924  sbcim1  2925  sbcbi1  2926  sbeqalb  2933  sbcel21v  2941  eqrd  3081  exmidsssn  4085  exmidsssnc  4086  copsexg  4126  euotd  4136  rexxfrd  4344  relop  4649  elres  4813  rnxpid  4931  relcnvtr  5016  iotaval  5057  mpteqb  5465  elfvmptrab  5470  chfnrn  5485  elpreima  5493  ffnfv  5532  f1elima  5628  f1eqcocnv  5646  fliftfun  5651  isoresbr  5664  isotr  5671  ovmpodv2  5858  smoiso  6153  nnaordi  6358  nnaword  6361  nnawordi  6365  xpider  6454  iinerm  6455  mptelixpg  6582  dom2lem  6620  nneneq  6704  exmidpw  6755  f1dmvrnfibi  6784  ismkvnex  6979  pr2nelem  6997  exmidfodomrlemeldju  7003  exmidfodomrlemreseldju  7004  addcanpig  7090  mulcanpig  7091  enqer  7114  ltexnqi  7165  prarloclemlo  7250  genpcdl  7275  genpcuu  7276  appdivnq  7319  ltprordil  7345  1idprl  7346  1idpru  7347  ltexprlemm  7356  ltexprlemopu  7359  ltexprlemru  7368  cauappcvgprlemladdru  7412  cauappcvgprlemladdrl  7413  caucvgprprlemopu  7455  caucvgsrlemoffcau  7540  caucvgsrlemoffres  7542  ltrenn  7590  axpre-ltadd  7621  addn0nid  8055  apne  8303  prodgt02  8521  prodge02  8523  mulgt1  8531  divgt0  8540  divge0  8541  cju  8629  nnsub  8669  nominpos  8861  zltnle  9004  nn0n0n1ge2  9025  zdcle  9031  btwnnz  9049  uzm1  9258  supinfneg  9292  infsupneg  9293  ublbneg  9307  cnref1o  9342  ltsubrp  9377  ltaddrp  9378  npnflt  9491  nmnfgt  9494  ge0nemnf  9500  xltnegi  9511  xnn0xadd0  9543  iccsupr  9642  icoshft  9666  iccshftri  9671  iccshftli  9673  iccdili  9675  icccntri  9677  fzdcel  9713  fznlem  9714  fzen  9716  fzofzim  9858  eluzgtdifelfzo  9867  elfzonelfzo  9900  qltnle  9916  addmodlteq  10064  fihashf1rn  10428  cjre  10547  caucvgre  10645  icodiamlt  10844  zsumdc  11045  reeff1  11258  dvds2lem  11353  muldvds1  11366  dvdscmulr  11370  dvdsmulcr  11371  dvdsdivcl  11396  oddnn02np1  11425  ndvdsadd  11476  zeqzmulgcd  11507  bezoutlemmain  11532  dfgcd2  11548  gcdmultiple  11554  coprmdvds  11619  divgcdodd  11667  isprm6  11671  prmdvdsexpr  11674  cncongrprm  11681  phiprmpw  11743  lmss  12257  cnplimcim  12592  dvcn  12619  ch2var  12665  bj-rspgt  12683  bj-nntrans  12839  bj-nnelirr  12841  bj-omtrans  12844  setindft  12853  bj-inf2vnlem3  12860  bj-inf2vnlem4  12861  bj-findis  12867