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

Metamath Proof Explorer

Theorem 3rspcedvdw

Description: Triple application of rspcedvdw . (Contributed by SN, 20-Aug-2024)

Ref Expression
Hypotheses 3rspcedvdw.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
3rspcedvdw.2 ⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜃 ) )
3rspcedvdw.3 ⊢ ( 𝑧 = 𝐶 → ( 𝜃 ↔ 𝜏 ) )
3rspcedvdw.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
3rspcedvdw.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
3rspcedvdw.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑍 )
3rspcedvdw.4 ⊢ ( 𝜑 → 𝜏 )
Assertion 3rspcedvdw ( 𝜑 → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ∃ 𝑧 ∈ 𝑍 𝜓 )

Proof

Step Hyp Ref Expression
1 3rspcedvdw.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
2 3rspcedvdw.2 ⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜃 ) )
3 3rspcedvdw.3 ⊢ ( 𝑧 = 𝐶 → ( 𝜃 ↔ 𝜏 ) )
4 3rspcedvdw.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
5 3rspcedvdw.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
6 3rspcedvdw.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑍 )
7 3rspcedvdw.4 ⊢ ( 𝜑 → 𝜏 )
8 1 2 3 rspc3ev ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ 𝜏 ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ∃ 𝑧 ∈ 𝑍 𝜓 )
9 4 5 6 7 8 syl31anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ∃ 𝑧 ∈ 𝑍 𝜓 )