MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspc3v Structured version   Visualization version   GIF version

Theorem rspc3v 3638
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
StepHypRef Expression
1 rspc3v.1 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜒))
21ralbidv 3178 . . . 4 (𝑥 = 𝐴 → (∀𝑧𝑇 𝜑 ↔ ∀𝑧𝑇 𝜒))
3 rspc3v.2 . . . . 5 (𝑦 = 𝐵 → (𝜒𝜃))
43ralbidv 3178 . . . 4 (𝑦 = 𝐵 → (∀𝑧𝑇 𝜒 ↔ ∀𝑧𝑇 𝜃))
52, 4rspc2v 3633 . . 3 ((𝐴𝑅𝐵𝑆) → (∀𝑥𝑅𝑦𝑆𝑧𝑇 𝜑 → ∀𝑧𝑇 𝜃))
6 rspc3v.3 . . . 4 (𝑧 = 𝐶 → (𝜃𝜓))
76rspcv 3618 . . 3 (𝐶𝑇 → (∀𝑧𝑇 𝜃𝜓))
85, 7sylan9 507 . 2 (((𝐴𝑅𝐵𝑆) ∧ 𝐶𝑇) → (∀𝑥𝑅𝑦𝑆𝑧𝑇 𝜑𝜓))
983impa 1110 1 ((𝐴𝑅𝐵𝑆𝐶𝑇) → (∀𝑥𝑅𝑦𝑆𝑧𝑇 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wcel 2108  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062
This theorem is referenced by:  rspc3dv  3641  rspc4v  3642  pocl  5600  swopolem  5602  isopolem  7365  caovassg  7631  caovcang  7634  caovordig  7638  caovordg  7640  caovdig  7647  caovdirg  7650  caofass  7737  caoftrn  7738  frpoins3xp3g  8166  prslem  18343  posi  18363  latdisdlem  18541  dlatmjdi  18568  sgrpass  18738  gaass  19315  rngdi  20157  rngdir  20158  o2timesd  20207  rglcom4d  20208  islmodd  20864  rmodislmodlem  20927  rmodislmod  20928  lsscl  20940  assalem  21877  psmettri2  24319  xmettri2  24350  addsproplem1  28002  addsprop  28009  axtgcgrid  28471  axtg5seg  28473  axtgpasch  28475  axtgupdim2  28479  axtgeucl  28480  tgdim01  28515  f1otrgitv  28878  grpoass  30522  vcdi  30584  vcdir  30585  vcass  30586  lnolin  30773  lnopl  31933  lnfnl  31950  omndadd  33083  axtgupdim2ALTV  34683  rngodi  37911  rngodir  37912  rngoass  37913  lfli  39062  cvlexch1  39329  isthincd2lem2  49084
  Copyright terms: Public domain W3C validator