Metamath Proof Explorer

Theorem 2ralbii

Description: Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004)

Ref Expression
Hypothesis ralbii.1 φ ψ
Assertion 2ralbii x A y B φ x A y B ψ


Step Hyp Ref Expression
1 ralbii.1 φ ψ
2 1 ralbii y B φ y B ψ
3 2 ralbii x A y B φ x A y B ψ