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 
|- ( ph -> A. x A. y ph )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( ph -> ph )
2 1 alrimivv 
 |-  ( ph -> A. x A. y ph )