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

Metamath Proof Explorer

Theorem 2ax5

Description: Quantification of two variables over a formula in which they do not occur. (Contributed by Alan Sare, 12-Apr-2011)

Ref Expression
Assertion 2ax5 ( 𝜑 → ∀ 𝑥 ∀ 𝑦 𝜑 )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝜑 → 𝜑 )
2 1 alrimivv ⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 𝜑 )