Metamath Proof Explorer


Theorem 2rspcedvdw

Description: Double application of rspcedvdw . (Contributed by SN, 24-Aug-2024)

Ref Expression
Hypotheses 2rspcedvdw.1 x = A ψ χ
2rspcedvdw.2 y = B χ θ
2rspcedvdw.a φ A X
2rspcedvdw.b φ B Y
2rspcedvdw.3 φ θ
Assertion 2rspcedvdw φ x X y Y ψ

Proof

Step Hyp Ref Expression
1 2rspcedvdw.1 x = A ψ χ
2 2rspcedvdw.2 y = B χ θ
3 2rspcedvdw.a φ A X
4 2rspcedvdw.b φ B Y
5 2rspcedvdw.3 φ θ
6 1 2 rspc2ev A X B Y θ x X y Y ψ
7 3 4 5 6 syl3anc φ x X y Y ψ