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 ⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
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 ⊢ (    𝜑    ,    𝜓    ▶    ∀ 𝑥 𝜒    )