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

Theorem rspc3v 3622
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 3167 . . . 4 (𝑥 = 𝐴 → (∀𝑧𝑇 𝜑 ↔ ∀𝑧𝑇 𝜒))
3 rspc3v.2 . . . . 5 (𝑦 = 𝐵 → (𝜒𝜃))
43ralbidv 3167 . . . 4 (𝑦 = 𝐵 → (∀𝑧𝑇 𝜒 ↔ ∀𝑧𝑇 𝜃))
52, 4rspc2v 3617 . . 3 ((𝐴𝑅𝐵𝑆) → (∀𝑥𝑅𝑦𝑆𝑧𝑇 𝜑 → ∀𝑧𝑇 𝜃))
6 rspc3v.3 . . . 4 (𝑧 = 𝐶 → (𝜃𝜓))
76rspcv 3602 . . 3 (𝐶𝑇 → (∀𝑧𝑇 𝜃𝜓))
85, 7sylan9 506 . 2 (((𝐴𝑅𝐵𝑆) ∧ 𝐶𝑇) → (∀𝑥𝑅𝑦𝑆𝑧𝑇 𝜑𝜓))
983impa 1107 1 ((𝐴𝑅𝐵𝑆𝐶𝑇) → (∀𝑥𝑅𝑦𝑆𝑧𝑇 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098  wral 3050
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 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051
This theorem is referenced by:  rspc3dv  3624  rspc4v  3625  pocl  5597  swopolem  5600  isopolem  7352  caovassg  7619  caovcang  7622  caovordig  7626  caovordg  7628  caovdig  7635  caovdirg  7638  caofass  7723  caoftrn  7724  frpoins3xp3g  8146  prslem  18293  posi  18312  latdisdlem  18491  dlatmjdi  18518  sgrpass  18688  gaass  19260  rngdi  20112  rngdir  20113  o2timesd  20162  rglcom4d  20163  islmodd  20761  rmodislmodlem  20824  rmodislmod  20825  rmodislmodOLD  20826  lsscl  20838  assalem  21808  psmettri2  24259  xmettri2  24290  addsproplem1  27932  addsprop  27939  axtgcgrid  28339  axtg5seg  28341  axtgpasch  28343  axtgupdim2  28347  axtgeucl  28348  tgdim01  28383  f1otrgitv  28746  grpoass  30385  vcdi  30447  vcdir  30448  vcass  30449  lnolin  30636  lnopl  31796  lnfnl  31813  omndadd  32876  axtgupdim2ALTV  34431  rngodi  37508  rngodir  37509  rngoass  37510  lfli  38663  cvlexch1  38930  isthincd2lem2  48228
  Copyright terms: Public domain W3C validator