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

Theorem 2eximdv 2015
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1929. (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 2013 . 2 (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒))
32eximdv 2013 1 (𝜑 → (∃𝑥𝑦𝜓 → ∃𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1875
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006
This theorem depends on definitions:  df-bi 199  df-ex 1876
This theorem is referenced by:  2eu6  2714  cgsex2g  3427  cgsex4g  3428  spc2egv  3483  spc3egv  3485  relop  5476  elinxp  5644  elresOLD  5646  en3  8439  en4  8440  addsrpr  10184  mulsrpr  10185  hash2prde  13501  pmtrrn2  18192  umgredg  26374  umgr2wlkon  27239  fundmpss  32178  pellexlem5  38183  ax6e2eq  39543  fnchoice  39948  fzisoeu  40259  stoweidlem35  40995  stoweidlem60  41020
  Copyright terms: Public domain W3C validator