Theorem syli 33

Description: Syllogism inference with common nested antecedent. (Contributed by NM, 4-Nov-2004.)

Hypotheses

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

Assertion

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

Proof of Theorem syli

Step	Hyp	Ref	Expression
1		syli.1	. 2 ⊢ (ψ → (φ → χ))
2		syli.2	. . 3 ⊢ (χ → (φ → θ))
3	2	com12 27	. 2 ⊢ (φ → (χ → θ))
4	1, 3	sylcom 25	1 ⊢ (ψ → (φ → θ))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  ibd  234  bija  344  eqpw1uni  4331  iss  5001  tz6.12c  5348