Metamath Proof Explorer


Theorem 3rspcedvd

Description: Triple application of rspcedvd . (Contributed by Steven Nguyen, 27-Feb-2023)

Ref Expression
Hypotheses 3rspcedvd.a φ A D
3rspcedvd.b φ B D
3rspcedvd.c φ C D
3rspcedvd.1 φ x = A ψ χ
3rspcedvd.2 φ y = B χ θ
3rspcedvd.3 φ z = C θ τ
3rspcedvd.4 φ τ
Assertion 3rspcedvd φ x D y D z D ψ

Proof

Step Hyp Ref Expression
1 3rspcedvd.a φ A D
2 3rspcedvd.b φ B D
3 3rspcedvd.c φ C D
4 3rspcedvd.1 φ x = A ψ χ
5 3rspcedvd.2 φ y = B χ θ
6 3rspcedvd.3 φ z = C θ τ
7 3rspcedvd.4 φ τ
8 4 2rexbidv φ x = A y D z D ψ y D z D χ
9 5 rexbidv φ y = B z D χ z D θ
10 3 6 7 rspcedvd φ z D θ
11 2 9 10 rspcedvd φ y D z D χ
12 1 8 11 rspcedvd φ x D y D z D ψ