Theorem sylibd 138

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 132	. 2 ⊢ (φ → (χ → θ))
4	1, 3	syld 40	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:  3imtr3d  191  dvelimdf  1874  ceqsalt  2557  sbceqal  2791  sbcimdv  2800  csbiebt  2863  rspcsbela  2882  preqr1g  3511  repizf2  3889  copsexg  3955  onun2  4166  suc11g  4219  elrnrexdm  5231  isoselem  5384  riotass2  5418  nnm00  6013  ecopovtrn  6114  ecopovtrng  6117  enq0tr  6289  addnqprl  6384  addnqpru  6385  mulnqprl  6412  mulnqpru  6413  recexprlemss1l  6469  recexprlemss1u  6470  cnegexlem1  6773  bj-peano4  7177