Theorem rspc3v 3573

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1541   ∈ wcel 2109  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070

This theorem is referenced by:  pocl  5509  swopolem  5512  isopolem  7209  caovassg  7461  caovcang  7464  caovordig  7468  caovordg  7470  caovdig  7477  caovdirg  7480  caofass  7561  caoftrn  7562  prslem  17997  posi  18016  latdisdlem  18195  dlatmjdi  18222  sgrpass  18362  gaass  18884  islmodd  20110  rmodislmodlem  20171  rmodislmod  20172  rmodislmodOLD  20173  lsscl  20185  assalem  21045  psmettri2  23443  xmettri2  23474  axtgcgrid  26805  axtg5seg  26807  axtgpasch  26809  axtgupdim2  26813  axtgeucl  26814  tgdim01  26849  f1otrgitv  27212  grpoass  28844  vcdi  28906  vcdir  28907  vcass  28908  lnolin  29095  lnopl  30255  lnfnl  30272  omndadd  31311  axtgupdim2ALTV  32627  frpoins3xp3g  33767  rngodi  36041  rngodir  36042  rngoass  36043  lfli  37054  cvlexch1  37321  rngdir  45392  isthincd2lem2  46269