Metamath Proof Explorer

Theorem 3albii

Description: Inference adding three universal quantifiers to both sides of an equivalence. (Contributed by Peter Mazsa, 10-Aug-2018)

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

Proof

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