Metamath Proof Explorer

Theorem ralbii

Description: Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994) (Revised by Mario Carneiro, 17-Oct-2016) (Proof shortened by Wolf Lammen, 4-Dec-2019)

Ref Expression
Hypothesis ralbii.1 φ ψ
Assertion ralbii x A φ x A ψ


Step Hyp Ref Expression
1 ralbii.1 φ ψ
2 1 imbi2i x A φ x A ψ
3 2 ralbii2 x A φ x A ψ