Theorem sylibd 148

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

Hypotheses

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

Assertion

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

Proof of Theorem sylibd

Step	Hyp	Ref	Expression
1		sylibd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylibd.2	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
3	2	biimpd 143	. 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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr3d  201  dvelimdf  1996  ceqsalt  2738  sbceqal  2992  csbiebt  3070  rspcsbela  3090  preqr1g  3729  repizf2  4123  copsexg  4204  onun2  4448  suc11g  4515  elrnrexdm  5605  isoselem  5767  riotass2  5803  oawordriexmid  6414  nnm00  6473  ecopovtrn  6574  ecopovtrng  6577  infglbti  6965  difinfsnlem  7037  enq0tr  7348  addnqprl  7443  addnqpru  7444  mulnqprl  7482  mulnqpru  7483  recexprlemss1l  7549  recexprlemss1u  7550  cauappcvgprlemdisj  7565  mulextsr1lem  7694  pitonn  7762  rereceu  7803  cnegexlem1  8044  ltadd2  8288  eqord2  8353  mulext  8483  mulgt1  8728  lt2halves  9062  addltmul  9063  nzadd  9213  zextlt  9250  recnz  9251  zeo  9263  peano5uzti  9266  irradd  9548  irrmul  9549  xltneg  9733  xleadd1  9772  icc0r  9823  fznuz  9997  uznfz  9998  facndiv  10606  rennim  10895  abs00ap  10955  absle  10982  cau3lem  11007  caubnd2  11010  climshft  11194  subcn2  11201  mulcn2  11202  serf0  11242  cvgratnnlemnexp  11414  cvgratnnlemmn  11415  efieq1re  11661  moddvds  11688  dvdsssfz1  11736  nn0seqcvgd  11909  algcvgblem  11917  eucalglt  11925  lcmgcdlem  11945  rpmul  11966  divgcdcoprm0  11969  isprm6  12012  rpexp  12018  eulerthlema  12093  eulerthlemh  12094  prmdiv  12098  tgss3  12449  cnpnei  12590  cnntr  12596  hmeoopn  12682  hmeocld  12683  mulcncflem  12961  sincosq3sgn  13120  sincosq4sgn  13121  bj-peano4  13501  iswomni0  13593