Metamath Proof Explorer


Theorem rexralbidv

Description: Formula-building rule for restricted quantifiers (deduction form). (Contributed by NM, 28-Jan-2006)

Ref Expression
Hypothesis 2rexbidv.1 φ ψ χ
Assertion rexralbidv φ x A y B ψ x A y B χ

Proof

Step Hyp Ref Expression
1 2rexbidv.1 φ ψ χ
2 1 ralbidv φ y B ψ y B χ
3 2 rexbidv φ x A y B ψ x A y B χ