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

Theorem reximddv2 3199
Description: Double deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019.)
Hypotheses
Ref Expression
reximddv2.1 ((((𝜑𝑥𝐴) ∧ 𝑦𝐵) ∧ 𝜓) → 𝜒)
reximddv2.2 (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜓)
Assertion
Ref Expression
reximddv2 (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜒)
Distinct variable groups:   𝑦,𝐴   𝜑,𝑥,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem reximddv2
StepHypRef Expression
1 reximddv2.1 . . . . 5 ((((𝜑𝑥𝐴) ∧ 𝑦𝐵) ∧ 𝜓) → 𝜒)
21ex 413 . . . 4 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32reximdva 3153 . . 3 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓 → ∃𝑦𝐵 𝜒))
43impr 455 . 2 ((𝜑 ∧ (𝑥𝐴 ∧ ∃𝑦𝐵 𝜓)) → ∃𝑦𝐵 𝜒)
5 reximddv2.2 . 2 (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜓)
64, 5reximddv 3156 1 (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2119  wrex 3064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065
This theorem is referenced by:  r19.29vva  3200  prmgaplem8  17027  cpmadugsumfi  22867  cpmidg2sum  22870  cayhamlem4  22878  ltgseg  28689  cgraswap  28913  cgracom  28915  cgratr  28916  flatcgra  28917  dfcgra2  28923  xrofsup  32866  elrlocbasi  33354  aks6d1c2  42622  prmunb2  44762
  Copyright terms: Public domain W3C validator