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

Theorem 2eximdv 1845
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1758. (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 1843 . 2 (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒))
32eximdv 1843 1 (𝜑 → (∃𝑥𝑦𝜓 → ∃𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836
This theorem depends on definitions:  df-bi 197  df-ex 1702
This theorem is referenced by:  2eu6  2557  cgsex2g  3225  cgsex4g  3226  spc2egv  3281  spc3egv  3283  relop  5232  elres  5394  en3  8141  en4  8142  addsrpr  9840  mulsrpr  9841  hash2prde  13190  pmtrrn2  17801  umgredg  25928  umgr2wlkon  26715  fundmpss  31365  pellexlem5  36874  ax6e2eq  38252  fnchoice  38668  fzisoeu  38975  stoweidlem35  39556  stoweidlem60  39581
  Copyright terms: Public domain W3C validator