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

Theorem reximddv2 3212
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 2105  wrex 3067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068
This theorem is referenced by:  r19.29vva  3213  r19.29vvaOLD  3214  prmgaplem8  17091  cpmadugsumfi  22898  cpmidg2sum  22901  cayhamlem4  22909  ltgseg  28618  cgraswap  28842  cgracom  28844  cgratr  28845  flatcgra  28846  dfcgra2  28852  xrofsup  32777  elrlocbasi  33252  aks6d1c2  42111  prmunb2  44306
  Copyright terms: Public domain W3C validator