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

Theorem reximdvva 3195
Description: Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by AV, 5-Jan-2022.)
Hypothesis
Ref Expression
ralimdvva.1 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝜓𝜒))
Assertion
Ref Expression
reximdvva (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 → ∃𝑥𝐴𝑦𝐵 𝜒))
Distinct variable groups:   𝑦,𝐴   𝑥,𝑦,𝜑
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem reximdvva
StepHypRef Expression
1 ralimdvva.1 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝜓𝜒))
21anassrs 466 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32reximdva 3157 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓 → ∃𝑦𝐵 𝜒))
43reximdva 3157 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 → ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wcel 2098  wrex 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-rex 3060
This theorem is referenced by:  reuop  6299  lcmgcdlem  16580  lsmelval2  20982  cpmadugsum  22824  mulsuniflem  28099  axpasch  28824  frgrwopreglem5  30203  frgrwopreglem5ALT  30204  eulerpartlemgvv  34127  cusgr3cyclex  34877  cvmlift2lem10  35053  ftc1anclem6  37302  hashnexinjle  41732  prprelprb  46994  reupr  46999
  Copyright terms: Public domain W3C validator