Metamath Proof Explorer


Theorem rexlim2d

Description: Inference removing two restricted quantifiers. Same as rexlimdvv , but with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses rexlim2d.x x φ
rexlim2d.y y φ
rexlim2d.3 φ x A y B ψ χ
Assertion rexlim2d φ x A y B ψ χ

Proof

Step Hyp Ref Expression
1 rexlim2d.x x φ
2 rexlim2d.y y φ
3 rexlim2d.3 φ x A y B ψ χ
4 nfv x χ
5 nfv y x A
6 2 5 nfan y φ x A
7 nfv y χ
8 3 expdimp φ x A y B ψ χ
9 6 7 8 rexlimd φ x A y B ψ χ
10 9 ex φ x A y B ψ χ
11 1 4 10 rexlimd φ x A y B ψ χ