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

Theorem 2eximdv 1835
 Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1751. (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 1833 . 2 (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒))
32eximdv 1833 1 (𝜑 → (∃𝑥𝑦𝜓 → ∃𝑥𝑦𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wex 1695 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827 This theorem depends on definitions:  df-bi 196  df-ex 1696 This theorem is referenced by:  2eu6  2546  cgsex2g  3212  cgsex4g  3213  spc2egv  3268  spc3egv  3270  relop  5194  elres  5355  en3  8082  en4  8083  addsrpr  9775  mulsrpr  9776  hash2prde  13109  pmtrrn2  17703  umgredg  25812  usgrarnedg  25913  fundmpss  30910  pellexlem5  36415  ax6e2eq  37794  fnchoice  38211  fzisoeu  38455  stoweidlem35  38928  stoweidlem60  38953  umgr2wlkon  41157
 Copyright terms: Public domain W3C validator