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

Theorem 2eximdv 1923
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1837. (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 1921 . 2 (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒))
32eximdv 1921 1 (𝜑 → (∃𝑥𝑦𝜓 → ∃𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-ex 1783
This theorem is referenced by:  2eu6  2653  cgsex2g  3520  cgsex4g  3521  cgsex4gOLD  3522  cgsex4gOLDOLD  3523  spc2egv  3590  rexopabb  5529  relop  5851  elinxp  6020  opreuopreu  8020  en3  9282  en4  9283  addsrpr  11070  mulsrpr  11071  hash2prde  14431  pmtrrn2  19328  umgredg  28398  umgr2wlkon  29204  trsp2cyc  32282  acycgrsubgr  34149  satfvsucsuc  34356  fmla0xp  34374  fundmpss  34738  pellexlem5  41571  ax6e2eq  43318  fnchoice  43713  fzisoeu  44010  stoweidlem35  44751  stoweidlem60  44776  or2expropbi  45744  ich2exprop  46139
  Copyright terms: Public domain W3C validator