Theorem rspc3ev 3596

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091

This theorem is used by:  3rspcedvdw  3597  f1dom3el3dif  7296  wrdl3s3  15144  pmltpclem1  25799  bdayfinbndlem1  28883  axlowdim  29569  axeuclidlem  29570  upgr3v3e3cycl  30811  br8d  33274  tgoldbachgt  35362  2goelgoanfmla1  36356  br8  36699  br6  36700  3dim1lem5  40715  lplni2  40786  3cubes  43893  jm2.27  44208  grimgrtri  49252  usgrexmpl1tri  49328