Theorem syl7 63

Description: A syllogism rule of inference. The first premise is used to replace the third antecedent of the second premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)

Hypotheses

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

Assertion

Ref	Expression
syl7	⊢ (χ → (θ → (φ → τ)))

Proof of Theorem syl7

Step	Hyp	Ref	Expression
1		syl7.1	. . 3 ⊢ (φ → ψ)
2	1	a1i 10	. 2 ⊢ (χ → (φ → ψ))
3		syl7.2	. 2 ⊢ (χ → (θ → (ψ → τ)))
4	2, 3	syl5d 62	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:  syl7bi  221  syl3an3  1217  ax10lem4  1941  hbae  1953  hbae-o  2153  ax11  2155  sfinltfin  4536