Theorem biimpd 132

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

Syntax hints:   → wi 4   ↔ wb 98

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

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  mpbid  135  sylibd  138  sylbid  139  mpbidi  140  syl5ib  143  syl6bi  152  ibi  165  imbi1d  220  biimpa  280  notbid  592  mtbird  598  mtbiri  600  orbi2d  704  pm3.37dc  788  pm5.15dc  1280  exlimd2  1486  exintr  1525  19.9d  1551  19.23t  1567  dral1  1618  spimt  1624  cbvalh  1636  chvar  1640  exdistrfor  1681  sbequi  1720  spv  1740  eqrdav  2039  cleqh  2137  ceqsalg  2582  vtoclf  2607  vtocl2  2609  vtocl3  2610  spcdv  2638  rspcdv  2659  elabgt  2684  sbeqalb  2815  eqrd  2963  copsexg  3981  euotd  3991  rexxfrd  4195  relop  4486  elres  4646  rnxpid  4755  relcnvtr  4840  iotaval  4878  mpteqb  5261  chfnrn  5278  elpreima  5286  ffnfv  5323  f1elima  5412  f1eqcocnv  5431  fliftfun  5436  isoresbr  5449  isotr  5456  ovmpt2dv2  5634  smoiso  5917  nnaordi  6081  nnaword  6084  nnawordi  6088  xpiderm  6177  iinerm  6178  dom2lem  6252  nneneq  6320  addcanpig  6432  mulcanpig  6433  enqer  6456  ltexnqi  6507  prarloclemlo  6592  genpcdl  6617  genpcuu  6618  appdivnq  6661  ltprordil  6687  1idprl  6688  1idpru  6689  ltexprlemm  6698  ltexprlemopu  6701  ltexprlemru  6710  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgprprlemopu  6797  caucvgsrlemoffcau  6882  caucvgsrlemoffres  6884  ltrenn  6931  axpre-ltadd  6960  apne  7614  prodgt02  7819  prodge02  7821  mulgt1  7829  divgt0  7838  divge0  7839  cju  7913  nnsub  7952  nominpos  8162  zltnle  8291  nn0n0n1ge2  8311  zdcle  8317  btwnnz  8334  uzm1  8503  ublbneg  8548  cnref1o  8582  ltsubrp  8617  ltaddrp  8618  ge0nemnf  8737  xltnegi  8748  iccsupr  8835  icoshft  8858  iccshftri  8863  iccshftli  8865  iccdili  8867  icccntri  8869  fzdcel  8904  fznlem  8905  fzen  8907  elfzmlbmOLD  8989  fzofzim  9044  eluzgtdifelfzo  9053  elfzonelfzo  9086  qltnle  9101  cjre  9482  caucvgre  9580  icodiamlt  9776  ch2var  9907  bj-rspgt  9925  bj-nntrans  10076  bj-nnelirr  10078  bj-omtrans  10081  setindft  10090  bj-inf2vnlem3  10097  bj-inf2vnlem4  10098  bj-findis  10104