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

Theorem 2eximdv 1878
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1796. (Contributed by NM, 3-Aug-1995.)
Hypothesis
Ref Expression
2alimdv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
2eximdv (𝜑 → (∃𝑥𝑦𝜓 → ∃𝑥𝑦𝜒))
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)

Proof of Theorem 2eximdv
StepHypRef Expression
1 2alimdv.1 . . 3 (𝜑 → (𝜓𝜒))
21eximdv 1876 . 2 (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒))
32eximdv 1876 1 (𝜑 → (∃𝑥𝑦𝜓 → ∃𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869
This theorem depends on definitions:  df-bi 199  df-ex 1743
This theorem is referenced by:  2eu6  2689  cgsex2g  3453  cgsex4g  3454  spc2egv  3512  relop  5565  elinxp  5729  opreuopreu  7540  en3  8544  en4  8545  addsrpr  10289  mulsrpr  10290  hash2prde  13633  pmtrrn2  18343  umgredg  26620  umgr2wlkon  27450  fmla0xp  32193  fundmpss  32529  pellexlem5  38826  ax6e2eq  40310  fnchoice  40705  fzisoeu  40996  stoweidlem35  41751  stoweidlem60  41776  or2expropbi  42674  ich2exprop  43001
  Copyright terms: Public domain W3C validator