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 3albii.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 3albii.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 )