Theorem rspc3ev 3628

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

Hypotheses

Ref	Expression
rspc3v.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
rspc3v.2	⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃))
rspc3v.3	⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓))

Assertion

Ref	Expression
rspc3ev	⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 ∃𝑧 ∈ 𝑇 𝜑)

Distinct variable groups:   𝜓,𝑧   𝜒,𝑥   𝜃,𝑦   𝑥,𝑦,𝑧,𝐴   𝑦,𝐵,𝑧   𝑧,𝐶   𝑥,𝑅   𝑥,𝑆,𝑦   𝑥,𝑇,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)   𝜓(𝑥,𝑦)   𝜒(𝑦,𝑧)   𝜃(𝑥,𝑧)   𝐵(𝑥)   𝐶(𝑥,𝑦)   𝑅(𝑦,𝑧)   𝑆(𝑧)

Proof of Theorem rspc3ev

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1089  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071

This theorem is referenced by:  f1dom3el3dif  7267  wrdl3s3  14912  pmltpclem1  24964  axlowdim  28216  axeuclidlem  28217  upgr3v3e3cycl  29430  br8d  31834  tgoldbachgt  33670  2goelgoanfmla1  34410  br8  34721  br6  34722  3dim1lem5  38332  lplni2  38403  3rspcedvdw  41032  3cubes  41418  jm2.27  41737