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  1991  ceqsalt  2712  sbceqal  2964  csbiebt  3039  rspcsbela  3059  preqr1g  3693  repizf2  4086  copsexg  4166  onun2  4406  suc11g  4472  elrnrexdm  5559  isoselem  5721  riotass2  5756  oawordriexmid  6366  nnm00  6425  ecopovtrn  6526  ecopovtrng  6529  infglbti  6912  difinfsnlem  6984  enq0tr  7242  addnqprl  7337  addnqpru  7338  mulnqprl  7376  mulnqpru  7377  recexprlemss1l  7443  recexprlemss1u  7444  cauappcvgprlemdisj  7459  mulextsr1lem  7588  pitonn  7656  rereceu  7697  cnegexlem1  7937  ltadd2  8181  eqord2  8246  mulext  8376  mulgt1  8621  lt2halves  8955  addltmul  8956  nzadd  9106  zextlt  9143  recnz  9144  zeo  9156  peano5uzti  9159  irradd  9438  irrmul  9439  xltneg  9619  xleadd1  9658  icc0r  9709  fznuz  9882  uznfz  9883  facndiv  10485  rennim  10774  abs00ap  10834  absle  10861  cau3lem  10886  caubnd2  10889  climshft  11073  subcn2  11080  mulcn2  11081  serf0  11121  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  efieq1re  11478  moddvds  11502  dvdsssfz1  11550  nn0seqcvgd  11722  algcvgblem  11730  eucalglt  11738  lcmgcdlem  11758  rpmul  11779  divgcdcoprm0  11782  isprm6  11825  rpexp  11831  tgss3  12247  cnpnei  12388  cnntr  12394  hmeoopn  12480  hmeocld  12481  mulcncflem  12759  sincosq3sgn  12909  sincosq4sgn  12910  bj-peano4  13153