This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ψ