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