This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to \forall x φ$
	alrimdh.2	$⊢ ψ \to \forall x ψ$
	alrimdh.3	$⊢ φ \to (ψ \to χ)$
Assertion	alrimdh	$⊢ φ \to (ψ \to \forall x χ)$

Proof

Step	Hyp	Ref	Expression
1		alrimdh.1	$⊢ φ \to \forall x φ$
2		alrimdh.2	$⊢ ψ \to \forall x ψ$
3		alrimdh.3	$⊢ φ \to (ψ \to χ)$
4	1 3	alimdh	$⊢ φ \to (\forall x ψ \to \forall x χ)$
5	2 4	syl5	$⊢ φ \to (ψ \to \forall x χ)$