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

Theorem rspc3ev 3574
Description: 3-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 25-Jul-2012.)
Hypotheses
Ref Expression
rspc3v.1 (𝑥 = 𝐴 → (𝜑𝜒))
rspc3v.2 (𝑦 = 𝐵 → (𝜒𝜃))
rspc3v.3 (𝑧 = 𝐶 → (𝜃𝜓))
Assertion
Ref Expression
rspc3ev (((𝐴𝑅𝐵𝑆𝐶𝑇) ∧ 𝜓) → ∃𝑥𝑅𝑦𝑆𝑧𝑇 𝜑)
Distinct variable groups:   𝜓,𝑧   𝜒,𝑥   𝜃,𝑦   𝑥,𝑦,𝑧,𝐴   𝑦,𝐵,𝑧   𝑧,𝐶   𝑥,𝑅   𝑥,𝑆,𝑦   𝑥,𝑇,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)   𝜓(𝑥,𝑦)   𝜒(𝑦,𝑧)   𝜃(𝑥,𝑧)   𝐵(𝑥)   𝐶(𝑥,𝑦)   𝑅(𝑦,𝑧)   𝑆(𝑧)

Proof of Theorem rspc3ev
StepHypRef Expression
1 simpl1 1190 . 2 (((𝐴𝑅𝐵𝑆𝐶𝑇) ∧ 𝜓) → 𝐴𝑅)
2 simpl2 1191 . 2 (((𝐴𝑅𝐵𝑆𝐶𝑇) ∧ 𝜓) → 𝐵𝑆)
3 rspc3v.3 . . . 4 (𝑧 = 𝐶 → (𝜃𝜓))
43rspcev 3561 . . 3 ((𝐶𝑇𝜓) → ∃𝑧𝑇 𝜃)
543ad2antl3 1186 . 2 (((𝐴𝑅𝐵𝑆𝐶𝑇) ∧ 𝜓) → ∃𝑧𝑇 𝜃)
6 rspc3v.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜒))
76rexbidv 3226 . . 3 (𝑥 = 𝐴 → (∃𝑧𝑇 𝜑 ↔ ∃𝑧𝑇 𝜒))
8 rspc3v.2 . . . 4 (𝑦 = 𝐵 → (𝜒𝜃))
98rexbidv 3226 . . 3 (𝑦 = 𝐵 → (∃𝑧𝑇 𝜒 ↔ ∃𝑧𝑇 𝜃))
107, 9rspc2ev 3572 . 2 ((𝐴𝑅𝐵𝑆 ∧ ∃𝑧𝑇 𝜃) → ∃𝑥𝑅𝑦𝑆𝑧𝑇 𝜑)
111, 2, 5, 10syl3anc 1370 1 (((𝐴𝑅𝐵𝑆𝐶𝑇) ∧ 𝜓) → ∃𝑥𝑅𝑦𝑆𝑧𝑇 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1539  wcel 2106  wrex 3065
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070
This theorem is referenced by:  f1dom3el3dif  7142  wrdl3s3  14677  pmltpclem1  24612  axlowdim  27329  axeuclidlem  27330  upgr3v3e3cycl  28544  br8d  30950  tgoldbachgt  32643  2goelgoanfmla1  33386  br8  33723  br6  33724  3dim1lem5  37480  lplni2  37551  3rspcedvdw  40181  3cubes  40512  jm2.27  40830
  Copyright terms: Public domain W3C validator