Theorem alrimdh

Description: Deduction form of Theorem 19.21 of Margaris p. 90, see 19.21 and 19.21h . (Contributed by NM, 10-Feb-1997) (Proof shortened by Andrew Salmon, 13-May-2011)

	Ref	Expression
Hypotheses	alrimdh.1	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
	alrimdh.2	⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
	alrimdh.3	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
Assertion	alrimdh	⊢ ( 𝜑 → ( 𝜓 → ∀ 𝑥 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		alrimdh.1	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		alrimdh.2	⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
3		alrimdh.3	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
4	1 3	alimdh	⊢ ( 𝜑 → ( ∀ 𝑥 𝜓 → ∀ 𝑥 𝜒 ) )
5	2 4	syl5	⊢ ( 𝜑 → ( 𝜓 → ∀ 𝑥 𝜒 ) )