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	1	rexbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑧 ∈ 𝑇 𝜑 ↔ ∃ 𝑧 ∈ 𝑇 𝜒 ) )
5	2	rexbidv	⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑧 ∈ 𝑇 𝜒 ↔ ∃ 𝑧 ∈ 𝑇 𝜃 ) )
6		simpl1	⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ 𝜓 ) → 𝐴 ∈ 𝑅 )
7		simpl2	⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ 𝜓 ) → 𝐵 ∈ 𝑆 )
8	3	rspcev	⊢ ( ( 𝐶 ∈ 𝑇 ∧ 𝜓 ) → ∃ 𝑧 ∈ 𝑇 𝜃 )
9	8	3ad2antl3	⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ 𝜓 ) → ∃ 𝑧 ∈ 𝑇 𝜃 )
10	4 5 6 7 9	2rspcedvdw	⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ 𝜓 ) → ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ∃ 𝑧 ∈ 𝑇 𝜑 )