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  1889  ceqsalt  2574  sbceqal  2808  sbcimdv  2817  csbiebt  2880  rspcsbela  2899  preqr1g  3528  repizf2  3906  copsexg  3972  onun2  4182  suc11g  4235  elrnrexdm  5249  isoselem  5402  riotass2  5437  nnm00  6038  ecopovtrn  6139  ecopovtrng  6142  enq0tr  6417  addnqprl  6512  addnqpru  6513  mulnqprl  6549  mulnqpru  6550  recexprlemss1l  6607  recexprlemss1u  6608  cauappcvgprlemdisj  6623  mulextsr1lem  6706  pitonn  6744  cnegexlem1  6983  ltadd2  7212  mulext  7398  mulgt1  7610  lt2halves  7937  addltmul  7938  zextlt  8108  recnz  8109  zeo  8119  peano5uzti  8122  irradd  8355  irrmul  8356  xltneg  8519  icc0r  8565  fznuz  8734  uznfz  8735  rennim  9211  bj-peano4  9415