Theorem syl7 69

Description: A syllogism rule of inference. The second premise is used to replace the third antecedent of the first 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 9	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
3		syl7.2	. 2 ⊢ (𝜒 → (𝜃 → (𝜓 → 𝜏)))
4	2, 3	syl5d 68	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:  syl7bi  165  syl3an3  1284  fvmptt  5656  nneneq  6927  pr2nelem  7270  ndvdssub  12112