Theorem rspc3ev 3624

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 1188	. 2 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → 𝐴 ∈ 𝑅)
2		simpl2 1189	. 2 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → 𝐵 ∈ 𝑆)
3		rspc3v.3	. . . 4 ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓))
4	3	rspcev 3607	. . 3 ⊢ ((𝐶 ∈ 𝑇 ∧ 𝜓) → ∃𝑧 ∈ 𝑇 𝜃)
5	4	3ad2antl3 1184	. 2 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → ∃𝑧 ∈ 𝑇 𝜃)
6		rspc3v.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
7	6	rexbidv 3169	. . 3 ⊢ (𝑥 = 𝐴 → (∃𝑧 ∈ 𝑇 𝜑 ↔ ∃𝑧 ∈ 𝑇 𝜒))
8		rspc3v.2	. . . 4 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃))
9	8	rexbidv 3169	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑧 ∈ 𝑇 𝜒 ↔ ∃𝑧 ∈ 𝑇 𝜃))
10	7, 9	rspc2ev 3620	. 2 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∃𝑧 ∈ 𝑇 𝜃) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 ∃𝑧 ∈ 𝑇 𝜑)
11	1, 2, 5, 10	syl3anc 1368	1 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 ∃𝑧 ∈ 𝑇 𝜑)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3052  df-rex 3061

This theorem is referenced by:  f1dom3el3dif  7277  wrdl3s3  14945  pmltpclem1  25407  axlowdim  28828  axeuclidlem  28829  upgr3v3e3cycl  30046  br8d  32457  tgoldbachgt  34365  2goelgoanfmla1  35104  br8  35420  br6  35421  3dim1lem5  39008  lplni2  39079  3rspcedvdw  41771  3cubes  42175  jm2.27  42494