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

Metamath Proof Explorer

Theorem rspc3ev

Description: 3-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 25-Jul-2012)

Ref Expression
Hypotheses rspc3v.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
rspc3v.2 ⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜃 ) )
rspc3v.3 ⊢ ( 𝑧 = 𝐶 → ( 𝜃 ↔ 𝜓 ) )
Assertion rspc3ev ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ 𝜓 ) → ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ∃ 𝑧 ∈ 𝑇 𝜑 )

Proof

Step Hyp Ref Expression
1 rspc3v.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
2 rspc3v.2 ⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜃 ) )
3 rspc3v.3 ⊢ ( 𝑧 = 𝐶 → ( 𝜃 ↔ 𝜓 ) )
4 simpl1 ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ 𝜓 ) → 𝐴 ∈ 𝑅 )
5 simpl2 ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ 𝜓 ) → 𝐵 ∈ 𝑆 )
6 3 rspcev ⊢ ( ( 𝐶 ∈ 𝑇 ∧ 𝜓 ) → ∃ 𝑧 ∈ 𝑇 𝜃 )
7 6 3ad2antl3 ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ 𝜓 ) → ∃ 𝑧 ∈ 𝑇 𝜃 )
8 1 rexbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑧 ∈ 𝑇 𝜑 ↔ ∃ 𝑧 ∈ 𝑇 𝜒 ) )
9 2 rexbidv ⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑧 ∈ 𝑇 𝜒 ↔ ∃ 𝑧 ∈ 𝑇 𝜃 ) )
10 8 9 rspc2ev ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝑇 𝜃 ) → ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ∃ 𝑧 ∈ 𝑇 𝜑 )
11 4 5 7 10 syl3anc ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ 𝜓 ) → ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ∃ 𝑧 ∈ 𝑇 𝜑 )