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

Theorem rspc4v 3630
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 1088 . . 3 ((𝐴𝑅𝐵𝑆𝐶𝑇) ↔ ((𝐴𝑅𝐵𝑆) ∧ 𝐶𝑇))
2 rspc4v.1 . . . . . 6 (𝑥 = 𝐴 → (𝜑𝜒))
32ralbidv 3176 . . . . 5 (𝑥 = 𝐴 → (∀𝑤𝑈 𝜑 ↔ ∀𝑤𝑈 𝜒))
4 rspc4v.2 . . . . . 6 (𝑦 = 𝐵 → (𝜒𝜃))
54ralbidv 3176 . . . . 5 (𝑦 = 𝐵 → (∀𝑤𝑈 𝜒 ↔ ∀𝑤𝑈 𝜃))
6 rspc4v.3 . . . . . 6 (𝑧 = 𝐶 → (𝜃𝜏))
76ralbidv 3176 . . . . 5 (𝑧 = 𝐶 → (∀𝑤𝑈 𝜃 ↔ ∀𝑤𝑈 𝜏))
83, 5, 7rspc3v 3627 . . . 4 ((𝐴𝑅𝐵𝑆𝐶𝑇) → (∀𝑥𝑅𝑦𝑆𝑧𝑇𝑤𝑈 𝜑 → ∀𝑤𝑈 𝜏))
9 rspc4v.4 . . . . 5 (𝑤 = 𝐷 → (𝜏𝜓))
109rspcv 3608 . . . 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 1086   = wceq 1540  wcel 2105  wral 3060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1088  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061
This theorem is referenced by:  rspc6v  3631  rspc8v  3632
  Copyright terms: Public domain W3C validator