Theorem rspc3v 3584

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 3162	. . . 4 ⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑇 𝜑 ↔ ∀𝑧 ∈ 𝑇 𝜒))
3		rspc3v.2	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃))
4	3	ralbidv 3162	. . . 4 ⊢ (𝑦 = 𝐵 → (∀𝑧 ∈ 𝑇 𝜒 ↔ ∀𝑧 ∈ 𝑇 𝜃))
5	2, 4	rspc2v 3581	. . 3 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → ∀𝑧 ∈ 𝑇 𝜃))
6		rspc3v.3	. . . 4 ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓))
7	6	rspcv 3566	. . 3 ⊢ (𝐶 ∈ 𝑇 → (∀𝑧 ∈ 𝑇 𝜃 → 𝜓))
8	5, 7	sylan9 511	. 2 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → 𝜓))
9	8	3impa 1107	1 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∀wral 3106

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-cleq 2791  df-clel 2870  df-ral 3111

This theorem is referenced by:  swopolem  5447  isopolem  7077  caovassg  7326  caovcang  7329  caovordig  7333  caovordg  7335  caovdig  7342  caovdirg  7345  caofass  7423  caoftrn  7424  prslem  17533  posi  17552  latdisdlem  17791  dlatmjdi  17796  sgrpass  17899  gaass  18419  islmodd  19633  rmodislmodlem  19694  rmodislmod  19695  lsscl  19707  assalem  20546  psmettri2  22916  xmettri2  22947  axtgcgrid  26257  axtg5seg  26259  axtgpasch  26261  axtgupdim2  26265  axtgeucl  26266  tgdim01  26301  f1otrgitv  26664  grpoass  28286  vcdi  28348  vcdir  28349  vcass  28350  lnolin  28537  lnopl  29697  lnfnl  29714  omndadd  30757  axtgupdim2ALTV  32049  rngodi  35342  rngodir  35343  rngoass  35344  lfli  36357  cvlexch1  36624  rngdir  44506