Metamath Proof Explorer

Theorem albii

Description: Inference adding universal quantifier to both sides of an equivalence. (Contributed by NM, 7-Aug-1994)

Ref Expression
Hypothesis albii.1 φ ψ
Assertion albii x φ x ψ


Step Hyp Ref Expression
1 albii.1 φ ψ
2 albi x φ ψ x φ x ψ
3 2 1 mpg x φ x ψ