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

Theorem 2eximdv 1919
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1834. (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 1917 . 2 (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒))
32eximdv 1917 1 (𝜑 → (∃𝑥𝑦𝜓 → ∃𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-ex 1780
This theorem is referenced by:  2eu6  2657  cgsex2g  3527  cgsex4g  3528  cgsex4gOLD  3529  spc2egv  3599  rexopabb  5533  relop  5861  elinxp  6037  opreuopreu  8059  en3  9316  en4  9317  addsrpr  11115  mulsrpr  11116  hash2prde  14509  hash3tpde  14532  pmtrrn2  19478  umgredg  29155  umgr2wlkon  29970  trsp2cyc  33143  acycgrsubgr  35163  satfvsucsuc  35370  fmla0xp  35388  fundmpss  35767  pellexlem5  42844  ax6e2eq  44577  fnchoice  45034  fzisoeu  45312  stoweidlem35  46050  stoweidlem60  46075  or2expropbi  47046  ich2exprop  47458
  Copyright terms: Public domain W3C validator