Metamath Proof Explorer

Theorem 2albii

Description: Inference adding two universal quantifiers to both sides of an equivalence. (Contributed by NM, 9-Mar-1997)

Ref Expression
Hypothesis albii.1 
|- ( ph <-> ps )
Assertion 2albii 
|- ( A. x A. y ph <-> A. x A. y ps )

Proof

Step Hyp Ref Expression
1 albii.1 
 |-  ( ph <-> ps )
2 1 albii 
 |-  ( A. y ph <-> A. y ps )
3 2 albii 
 |-  ( A. x A. y ph <-> A. x A. y ps )