Theorem syl3c 57

Description: A syllogism inference combined with contraction. e111 without virtual deductions. (Contributed by Alan Sare, 7-Jul-2011.)

Hypotheses

Ref	Expression
syl3c.1	⊢ (φ → ψ)
syl3c.2	⊢ (φ → χ)
syl3c.3	⊢ (φ → θ)
syl3c.4	⊢ (ψ → (χ → (θ → τ)))

Assertion

Ref	Expression
syl3c	⊢ (φ → τ)

Proof of Theorem syl3c

Step	Hyp	Ref	Expression
1		syl3c.3	. 2 ⊢ (φ → θ)
2		syl3c.1	. . 3 ⊢ (φ → ψ)
3		syl3c.2	. . 3 ⊢ (φ → χ)
4		syl3c.4	. . 3 ⊢ (ψ → (χ → (θ → τ)))
5	2, 3, 4	sylc 56	. 2 ⊢ (φ → (θ → τ))
6	1, 5	mpd 14	1 ⊢ (φ → τ)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  extd  5924  symd  5925  nchoicelem19  6308