Theorem sylibrd 167

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylibrd.1	⊢ (𝜑 → (𝜓 → 𝜒))
sylibrd.2	⊢ (𝜑 → (𝜃 ↔ 𝜒))

Assertion

Ref	Expression
sylibrd	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem sylibrd

Step	Hyp	Ref	Expression
1		sylibrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylibrd.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
3	2	biimprd 156	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 44	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  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3imtr4d  201  sbciegft  2867  opeldmg  4629  elreldm  4649  ssimaex  5349  resflem  5446  f1eqcocnv  5552  fliftfun  5557  isopolem  5583  isosolem  5585  brtposg  6001  issmo2  6036  nnmcl  6224  nnawordi  6254  nnmordi  6255  nnmord  6256  swoord1  6301  ecopovtrn  6369  ecopovtrng  6372  f1domg  6455  mapen  6542  mapxpen  6544  supmoti  6667  isotilem  6680  exmidomniim  6776  enq0tr  6972  prubl  7024  ltexprlemloc  7145  addextpr  7159  recexprlem1ssl  7171  recexprlem1ssu  7172  cauappcvgprlemdisj  7189  mulcmpblnr  7266  mulgt0sr  7302  ltleletr  7546  ltle  7551  ltadd2  7876  leltadd  7904  reapti  8032  apreap  8040  reapcotr  8051  apcotr  8060  addext  8063  mulext1  8065  zapne  8791  zextle  8807  prime  8815  uzin  9020  indstr  9050  supinfneg  9052  infsupneg  9053  ublbneg  9067  xrltle  9237  xrre2  9252  icc0r  9313  fzrevral  9486  flqge  9654  modqadd1  9733  modqmul1  9749  facdiv  10111  resqrexlemgt0  10418  abs00ap  10460  absext  10461  climshftlemg  10654  climcaucn  10704  dvds2lem  10890  dvdsfac  10943  ltoddhalfle  10975  ndvdsadd  11013  gcdaddm  11057  bezoutlembi  11076  gcdzeq  11093  ialgcvga  11115  rpdvds  11163  cncongr1  11167  cncongr2  11168  prmind2  11184  euclemma  11207  isprm6  11208  rpexp  11214  sqrt2irr  11223