Theorem syl1 16

Description: A closed form of syllogism. Theorem *2.05 of [WhiteheadRussell] p. 100.

Assertion

Ref	Expression
syl1	⊢ ((φ → ψ) → ((χ → φ) → (χ → ψ)))

Proof of Theorem syl1

Step	Hyp	Ref	Expression
1		ax-1 3	. 2 ⊢ ((φ → ψ) → (χ → (φ → ψ)))
2	1	a2d 15	1 ⊢ ((φ → ψ) → ((χ → φ) → (χ → ψ)))

Syntax hints:   → wi 2

This theorem is referenced by:  syl2 17  syldd 50  pm2.36 91  pm2.61 109  osumlem4 5533

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org