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

Theorem 2eximdv 1917
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1831. (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 1915 . 2 (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒))
32eximdv 1915 1 (𝜑 → (∃𝑥𝑦𝜓 → ∃𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908
This theorem depends on definitions:  df-bi 207  df-ex 1777
This theorem is referenced by:  2eu6  2655  cgsex2g  3525  cgsex4g  3526  cgsex4gOLD  3527  spc2egv  3599  rexopabb  5538  relop  5864  elinxp  6039  opreuopreu  8058  en3  9314  en4  9315  addsrpr  11113  mulsrpr  11114  hash2prde  14506  hash3tpde  14529  pmtrrn2  19493  umgredg  29170  umgr2wlkon  29980  trsp2cyc  33126  acycgrsubgr  35143  satfvsucsuc  35350  fmla0xp  35368  fundmpss  35748  pellexlem5  42821  ax6e2eq  44555  fnchoice  44967  fzisoeu  45251  stoweidlem35  45991  stoweidlem60  46016  or2expropbi  46984  ich2exprop  47396
  Copyright terms: Public domain W3C validator