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

Theorem rspc3v 3639
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 3201 . . . 4 (𝑥 = 𝐴 → (∀𝑧𝑇 𝜑 ↔ ∀𝑧𝑇 𝜒))
3 rspc3v.2 . . . . 5 (𝑦 = 𝐵 → (𝜒𝜃))
43ralbidv 3201 . . . 4 (𝑦 = 𝐵 → (∀𝑧𝑇 𝜒 ↔ ∀𝑧𝑇 𝜃))
52, 4rspc2v 3636 . . 3 ((𝐴𝑅𝐵𝑆) → (∀𝑥𝑅𝑦𝑆𝑧𝑇 𝜑 → ∀𝑧𝑇 𝜃))
6 rspc3v.3 . . . 4 (𝑧 = 𝐶 → (𝜃𝜓))
76rspcv 3621 . . 3 (𝐶𝑇 → (∀𝑧𝑇 𝜃𝜓))
85, 7sylan9 508 . 2 (((𝐴𝑅𝐵𝑆) ∧ 𝐶𝑇) → (∀𝑥𝑅𝑦𝑆𝑧𝑇 𝜑𝜓))
983impa 1104 1 ((𝐴𝑅𝐵𝑆𝐶𝑇) → (∀𝑥𝑅𝑦𝑆𝑧𝑇 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wcel 2107  wral 3142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1083  df-ex 1774  df-cleq 2818  df-clel 2897  df-ral 3147
This theorem is referenced by:  swopolem  5481  isopolem  7093  caovassg  7339  caovcang  7342  caovordig  7346  caovordg  7348  caovdig  7355  caovdirg  7358  caofass  7436  caoftrn  7437  prslem  17533  posi  17552  latdisdlem  17791  dlatmjdi  17796  sgrpass  17898  gaass  18359  islmodd  19562  rmodislmodlem  19623  rmodislmod  19624  lsscl  19636  assalem  20010  psmettri2  22834  xmettri2  22865  axtgcgrid  26163  axtg5seg  26165  axtgpasch  26167  axtgupdim2  26171  axtgeucl  26172  tgdim01  26207  f1otrgitv  26570  grpoass  28194  vcdi  28256  vcdir  28257  vcass  28258  lnolin  28445  lnopl  29605  lnfnl  29622  omndadd  30621  axtgupdim2ALTV  31825  rngodi  35050  rngodir  35051  rngoass  35052  lfli  36064  cvlexch1  36331  rngdir  43981
  Copyright terms: Public domain W3C validator