Theorem sylibrd 168

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 157	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 45	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  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr4d  202  sbciegft  2939  opeldmg  4744  elreldm  4765  ssimaex  5482  resflem  5584  f1eqcocnv  5692  fliftfun  5697  isopolem  5723  isosolem  5725  brtposg  6151  issmo2  6186  nnmcl  6377  nnawordi  6411  nnmordi  6412  nnmord  6413  swoord1  6458  ecopovtrn  6526  ecopovtrng  6529  f1domg  6652  mapen  6740  mapxpen  6742  supmoti  6880  isotilem  6893  exmidomniim  7013  enq0tr  7242  prubl  7294  ltexprlemloc  7415  addextpr  7429  recexprlem1ssl  7441  recexprlem1ssu  7442  cauappcvgprlemdisj  7459  mulcmpblnr  7549  mulgt0sr  7586  map2psrprg  7613  ltleletr  7846  ltle  7851  ltadd2  8181  leltadd  8209  reapti  8341  apreap  8349  reapcotr  8360  apcotr  8369  addext  8372  mulext1  8374  cnstab  8407  zapne  9125  zextle  9142  prime  9150  uzin  9358  indstr  9388  supinfneg  9390  infsupneg  9391  ublbneg  9405  xrltle  9584  xrre2  9604  icc0r  9709  fzrevral  9885  flqge  10055  modqadd1  10134  modqmul1  10150  facdiv  10484  resqrexlemgt0  10792  abs00ap  10834  absext  10835  climshftlemg  11071  climcaucn  11120  dvds2lem  11505  dvdsfac  11558  ltoddhalfle  11590  ndvdsadd  11628  gcdaddm  11672  bezoutlembi  11693  gcdzeq  11710  algcvga  11732  rpdvds  11780  cncongr1  11784  cncongr2  11785  prmind2  11801  euclemma  11824  isprm6  11825  rpexp  11831  sqrt2irr  11840  fiinbas  12216  bastg  12230  tgcl  12233  opnssneib  12325  tgcnp  12378  iscnp4  12387  cnntr  12394  cnptopresti  12407  lmss  12415  lmtopcnp  12419  txdis  12446  xblss2ps  12573  xblss2  12574  blsscls2  12662  metequiv2  12665  bdxmet  12670  mulc1cncf  12745  cncfco  12747  sincosq2sgn  12908  sincosq3sgn  12909  sincosq4sgn  12910  triap  13224