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

Metamath Proof Explorer

Theorem gen21nv

Description: Virtual deduction form of alrimdh . (Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	gen21nv.1	$⊢ φ \to \forall x φ$
	gen21nv.2	$⊢ ψ \to \forall x ψ$
	gen21nv.3	$⊢ (φ, ψ \to χ)$
Assertion	gen21nv	$⊢ (φ, ψ \to \forall x χ)$

Proof

Step	Hyp	Ref	Expression
1		gen21nv.1	$⊢ φ \to \forall x φ$
2		gen21nv.2	$⊢ ψ \to \forall x ψ$
3		gen21nv.3	$⊢ (φ, ψ \to χ)$
4	3	dfvd2i	$⊢ φ \to (ψ \to χ)$
5	1 2 4	alrimdh	$⊢ φ \to (ψ \to \forall x χ)$
6	5	dfvd2ir	$⊢ (φ, ψ \to \forall x χ)$