Metamath Proof Explorer


Theorem rspc2dv

Description: 2-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 6-Mar-2025)

Ref Expression
Hypotheses rspc2dv.1 x = A ψ θ
rspc2dv.2 y = B θ χ
rspc2dv.3 φ x C y D ψ
rspc2dv.4 φ A C
rspc2dv.5 φ B D
Assertion rspc2dv φ χ

Proof

Step Hyp Ref Expression
1 rspc2dv.1 x = A ψ θ
2 rspc2dv.2 y = B θ χ
3 rspc2dv.3 φ x C y D ψ
4 rspc2dv.4 φ A C
5 rspc2dv.5 φ B D
6 1 2 rspc2va A C B D x C y D ψ χ
7 4 5 3 6 syl21anc φ χ