Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alan Sare
Virtual Deduction Theorems
gen21nv
Metamath Proof Explorer
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
⊢ ( 𝜑 , 𝜓 ▶ ∀ 𝑥 𝜒 )