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 φ ψ
Assertion 3albii x y z φ x y z ψ

Proof

Step Hyp Ref Expression
1 3albii.1 φ ψ
2 1 2albii y z φ y z ψ
3 2 albii x y z φ x y z ψ