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	⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ 𝜓 ) → ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ∃ 𝑧 ∈ 𝑇 𝜑 )