Theorem rspc3v 2884

Description: 3-variable restricted specialization, using implicit substitution. (Contributed by NM, 10-May-2005.)

Hypotheses

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

Assertion

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

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

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

Proof of Theorem rspc3v

Step	Hyp	Ref	Expression
1		rspc3v.1	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2	1	ralbidv 2497	. . . 4 ⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑇 𝜑 ↔ ∀𝑧 ∈ 𝑇 𝜒))
3		rspc3v.2	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃))
4	3	ralbidv 2497	. . . 4 ⊢ (𝑦 = 𝐵 → (∀𝑧 ∈ 𝑇 𝜒 ↔ ∀𝑧 ∈ 𝑇 𝜃))
5	2, 4	rspc2v 2881	. . 3 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → ∀𝑧 ∈ 𝑇 𝜃))
6		rspc3v.3	. . . 4 ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓))
7	6	rspcv 2864	. . 3 ⊢ (𝐶 ∈ 𝑇 → (∀𝑧 ∈ 𝑇 𝜃 → 𝜓))
8	5, 7	sylan9 409	. 2 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → 𝜓))
9	8	3impa 1196	1 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → 𝜓))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 980   = wceq 1364   ∈ wcel 2167  ∀wral 2475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-v 2765

This theorem is referenced by:  swopolem  4340  isopolem  5869  isosolem  5871  caovassg  6082  caovcang  6085  caovordig  6089  caovordg  6091  caovdig  6098  caovdirg  6101  caoftrn  6163  sgrpass  13051  rngdi  13496  rngdir  13497  islmodd  13849  rmodislmodlem  13906  rmodislmod  13907  lssclg  13920  psmettri2  14564  xmettri2  14597