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

Theorem rspc3v 3628
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 3623 . . 3 ((𝐴𝑅𝐵𝑆) → (∀𝑥𝑅𝑦𝑆𝑧𝑇 𝜑 → ∀𝑧𝑇 𝜃))
6 rspc3v.3 . . . 4 (𝑧 = 𝐶 → (𝜃𝜓))
76rspcv 3609 . . 3 (𝐶𝑇 → (∀𝑧𝑇 𝜃𝜓))
85, 7sylan9 509 . 2 (((𝐴𝑅𝐵𝑆) ∧ 𝐶𝑇) → (∀𝑥𝑅𝑦𝑆𝑧𝑇 𝜑𝜓))
983impa 1111 1 ((𝐴𝑅𝐵𝑆𝐶𝑇) → (∀𝑥𝑅𝑦𝑆𝑧𝑇 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wcel 2107  wral 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063
This theorem is referenced by:  rspc3dv  3630  rspc4v  3631  pocl  5596  swopolem  5599  isopolem  7342  caovassg  7605  caovcang  7608  caovordig  7612  caovordg  7614  caovdig  7621  caovdirg  7624  caofass  7707  caoftrn  7708  frpoins3xp3g  8127  prslem  18251  posi  18270  latdisdlem  18449  dlatmjdi  18476  sgrpass  18616  gaass  19161  o2timesd  20033  rglcom4d  20034  islmodd  20477  rmodislmodlem  20539  rmodislmod  20540  rmodislmodOLD  20541  lsscl  20553  assalem  21412  psmettri2  23815  xmettri2  23846  addsproplem1  27453  addsprop  27460  axtgcgrid  27714  axtg5seg  27716  axtgpasch  27718  axtgupdim2  27722  axtgeucl  27723  tgdim01  27758  f1otrgitv  28121  grpoass  29756  vcdi  29818  vcdir  29819  vcass  29820  lnolin  30007  lnopl  31167  lnfnl  31184  omndadd  32224  axtgupdim2ALTV  33680  rngodi  36772  rngodir  36773  rngoass  36774  lfli  37931  cvlexch1  38198  rngdi  46659  rngdir  46660  isthincd2lem2  47656
  Copyright terms: Public domain W3C validator