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

Theorem rspc4v 3625
Description: 4-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 7-Feb-2025.)
Hypotheses
Ref Expression
rspc4v.1 (𝑥 = 𝐴 → (𝜑𝜒))
rspc4v.2 (𝑦 = 𝐵 → (𝜒𝜃))
rspc4v.3 (𝑧 = 𝐶 → (𝜃𝜏))
rspc4v.4 (𝑤 = 𝐷 → (𝜏𝜓))
Assertion
Ref Expression
rspc4v (((𝐴𝑅𝐵𝑆) ∧ (𝐶𝑇𝐷𝑈)) → (∀𝑥𝑅𝑦𝑆𝑧𝑇𝑤𝑈 𝜑𝜓))
Distinct variable groups:   𝑤,𝐴,𝑥,𝑦,𝑧   𝑤,𝐵,𝑦,𝑧   𝑤,𝐶,𝑧   𝑤,𝐷   𝑥,𝑅   𝑥,𝑆,𝑦   𝑥,𝑇,𝑦,𝑧   𝑤,𝑈,𝑥,𝑦,𝑧   𝜒,𝑥   𝜓,𝑤   𝜏,𝑧   𝜃,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤)   𝜓(𝑥,𝑦,𝑧)   𝜒(𝑦,𝑧,𝑤)   𝜃(𝑥,𝑧,𝑤)   𝜏(𝑥,𝑦,𝑤)   𝐵(𝑥)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦,𝑧)   𝑅(𝑦,𝑧,𝑤)   𝑆(𝑧,𝑤)   𝑇(𝑤)

Proof of Theorem rspc4v
StepHypRef Expression
1 df-3an 1086 . . 3 ((𝐴𝑅𝐵𝑆𝐶𝑇) ↔ ((𝐴𝑅𝐵𝑆) ∧ 𝐶𝑇))
2 rspc4v.1 . . . . . 6 (𝑥 = 𝐴 → (𝜑𝜒))
32ralbidv 3171 . . . . 5 (𝑥 = 𝐴 → (∀𝑤𝑈 𝜑 ↔ ∀𝑤𝑈 𝜒))
4 rspc4v.2 . . . . . 6 (𝑦 = 𝐵 → (𝜒𝜃))
54ralbidv 3171 . . . . 5 (𝑦 = 𝐵 → (∀𝑤𝑈 𝜒 ↔ ∀𝑤𝑈 𝜃))
6 rspc4v.3 . . . . . 6 (𝑧 = 𝐶 → (𝜃𝜏))
76ralbidv 3171 . . . . 5 (𝑧 = 𝐶 → (∀𝑤𝑈 𝜃 ↔ ∀𝑤𝑈 𝜏))
83, 5, 7rspc3v 3622 . . . 4 ((𝐴𝑅𝐵𝑆𝐶𝑇) → (∀𝑥𝑅𝑦𝑆𝑧𝑇𝑤𝑈 𝜑 → ∀𝑤𝑈 𝜏))
9 rspc4v.4 . . . . 5 (𝑤 = 𝐷 → (𝜏𝜓))
109rspcv 3602 . . . 4 (𝐷𝑈 → (∀𝑤𝑈 𝜏𝜓))
118, 10sylan9 507 . . 3 (((𝐴𝑅𝐵𝑆𝐶𝑇) ∧ 𝐷𝑈) → (∀𝑥𝑅𝑦𝑆𝑧𝑇𝑤𝑈 𝜑𝜓))
121, 11sylanbr 581 . 2 ((((𝐴𝑅𝐵𝑆) ∧ 𝐶𝑇) ∧ 𝐷𝑈) → (∀𝑥𝑅𝑦𝑆𝑧𝑇𝑤𝑈 𝜑𝜓))
1312anasss 466 1 (((𝐴𝑅𝐵𝑆) ∧ (𝐶𝑇𝐷𝑈)) → (∀𝑥𝑅𝑦𝑆𝑧𝑇𝑤𝑈 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1084   = wceq 1533  wcel 2098  wral 3055
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 2697
This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1086  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-ral 3056
This theorem is referenced by:  rspc6v  3626  rspc8v  3627
  Copyright terms: Public domain W3C validator