Theorem biimpd 142

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 116	. 2 ⊢ ((𝜓 ↔ 𝜒) → (𝜓 → 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  mpbid  145  sylibd  147  sylbid  148  mpbidi  149  syl5ib  152  syl6bi  161  ibi  174  imbi1d  229  biimpa  290  notbid  624  mtbird  630  mtbiri  632  orbi2d  736  pm5.15dc  1320  exlimd2  1526  exintr  1565  19.9d  1591  19.23t  1607  dral1  1658  spimt  1664  cbvalh  1676  chvar  1680  exdistrfor  1721  sbequi  1760  spv  1781  eqrdav  2080  cleqh  2178  ceqsalg  2627  vtoclf  2652  vtocl2  2654  vtocl3  2655  spcdv  2683  rspcdv  2704  elabgt  2735  sbcn1  2861  sbcim1  2862  sbcbi1  2863  sbeqalb  2870  sbcel21v  2878  eqrd  3017  copsexg  3999  euotd  4009  rexxfrd  4213  relop  4504  elres  4664  rnxpid  4775  relcnvtr  4860  iotaval  4898  mpteqb  5282  chfnrn  5299  elpreima  5307  ffnfv  5344  f1elima  5433  f1eqcocnv  5451  fliftfun  5456  isoresbr  5469  isotr  5476  ovmpt2dv2  5654  smoiso  5940  nnaordi  6104  nnaword  6107  nnawordi  6111  xpiderm  6200  iinerm  6201  dom2lem  6275  nneneq  6343  f1dmvrnfibi  6393  pr2nelem  6460  addcanpig  6524  mulcanpig  6525  enqer  6548  ltexnqi  6599  prarloclemlo  6684  genpcdl  6709  genpcuu  6710  appdivnq  6753  ltprordil  6779  1idprl  6780  1idpru  6781  ltexprlemm  6790  ltexprlemopu  6793  ltexprlemru  6802  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  caucvgprprlemopu  6889  caucvgsrlemoffcau  6974  caucvgsrlemoffres  6976  ltrenn  7023  axpre-ltadd  7052  addn0nid  7478  apne  7723  prodgt02  7931  prodge02  7933  mulgt1  7941  divgt0  7950  divge0  7951  cju  8038  nnsub  8077  nominpos  8268  zltnle  8397  nn0n0n1ge2  8418  zdcle  8424  btwnnz  8441  uzm1  8649  supinfneg  8683  infsupneg  8684  ublbneg  8698  cnref1o  8733  ltsubrp  8768  ltaddrp  8769  ge0nemnf  8891  xltnegi  8902  iccsupr  8989  icoshft  9012  iccshftri  9017  iccshftli  9019  iccdili  9021  icccntri  9023  fzdcel  9059  fznlem  9060  fzen  9062  fzofzim  9197  eluzgtdifelfzo  9206  elfzonelfzo  9239  qltnle  9255  addmodlteq  9400  cjre  9769  caucvgre  9867  icodiamlt  10066  dvds2lem  10207  muldvds1  10220  dvdscmulr  10224  dvdsmulcr  10225  dvdsdivcl  10250  oddnn02np1  10280  ndvdsadd  10331  zeqzmulgcd  10362  bezoutlemmain  10387  dfgcd2  10403  gcdmultiple  10409  coprmdvds  10474  divgcdodd  10522  isprm6  10526  prmdvdsexpr  10529  cncongrprm  10536  ch2var  10578  bj-rspgt  10596  bj-nntrans  10746  bj-nnelirr  10748  bj-omtrans  10751  setindft  10760  bj-inf2vnlem3  10767  bj-inf2vnlem4  10768  bj-findis  10774