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

Theorem reximddv2 3209
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 412 . . . 4 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32reximdva 3165 . . 3 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓 → ∃𝑦𝐵 𝜒))
43impr 454 . 2 ((𝜑 ∧ (𝑥𝐴 ∧ ∃𝑦𝐵 𝜓)) → ∃𝑦𝐵 𝜒)
5 reximddv2.2 . 2 (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜓)
64, 5reximddv 3168 1 (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2099  wrex 3067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-rex 3068
This theorem is referenced by:  r19.29vva  3210  r19.29vvaOLD  3211  prmgaplem8  17026  cpmadugsumfi  22778  cpmidg2sum  22781  cayhamlem4  22789  ltgseg  28399  cgraswap  28623  cgracom  28625  cgratr  28626  flatcgra  28627  dfcgra2  28633  xrofsup  32537  elrlocbasi  32980  aks6d1c2  41601  prmunb2  43748
  Copyright terms: Public domain W3C validator