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	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
	gen21nv.2	⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
	gen21nv.3	⊢ (    𝜑    ,    𝜓    ▶    𝜒    )
Assertion	gen21nv	⊢ (    𝜑    ,    𝜓    ▶    ∀ 𝑥 𝜒    )

Proof

Step	Hyp	Ref	Expression
1		gen21nv.1	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		gen21nv.2	⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
3		gen21nv.3	⊢ (    𝜑    ,    𝜓    ▶    𝜒    )
4	3	dfvd2i	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
5	1 2 4	alrimdh	⊢ ( 𝜑 → ( 𝜓 → ∀ 𝑥 𝜒 ) )
6	5	dfvd2ir	⊢ (    𝜑    ,    𝜓    ▶    ∀ 𝑥 𝜒    )