Theorem sylbird 159

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

Hypotheses

Ref	Expression
sylbird.1	⊢ (φ → (χ ↔ ψ))
sylbird.2	⊢ (φ → (χ → θ))

Assertion

Ref	Expression
sylbird	⊢ (φ → (ψ → θ))

Proof of Theorem sylbird

Step	Hyp	Ref	Expression
1		sylbird.1	. . 3 ⊢ (φ → (χ ↔ ψ))
2	1	biimprd 147	. 2 ⊢ (φ → (ψ → χ))
3		sylbird.2	. 2 ⊢ (φ → (χ → θ))
4	2, 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  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3imtr3d  191  drex1  1676  eqreu  2727  onsucsssucr  4200  ordsucunielexmid  4216  ovi3  5579  tfrlem9  5876  rdgon  5913  dom2lem  6188  distrlem4prl  6560  distrlem4pru  6561  recexprlemm  6596  caucvgprlem1  6650  aptisr  6705  renegcl  7068  remulext2  7384  mulext1  7396  apmul1  7546  nnge1  7718  0mnnnnn0  7990  nn0lt2  8098  zneo  8115  uzind2  8126  fzind  8129  nn0ind-raph  8131  elfzmlbp  8760  difelfznle  8763  elfzodifsumelfzo  8827  ssfzo12  8850