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

Theorem 2eximdv 1920
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1835. (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 1918 . 2 (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒))
32eximdv 1918 1 (𝜑 → (∃𝑥𝑦𝜓 → ∃𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911
This theorem depends on definitions:  df-bi 210  df-ex 1782
This theorem is referenced by:  2eu6  2722  cgsex2g  3488  cgsex4g  3489  cgsex4gOLD  3490  spc2egv  3551  rexopabb  5383  relop  5689  elinxp  5860  opreuopreu  7720  en3  8743  en4  8744  addsrpr  10490  mulsrpr  10491  hash2prde  13828  pmtrrn2  18583  umgredg  26934  umgr2wlkon  27739  trsp2cyc  30818  acycgrsubgr  32513  satfvsucsuc  32720  fmla0xp  32738  fundmpss  33117  pellexlem5  39761  ax6e2eq  41250  fnchoice  41645  fzisoeu  41919  stoweidlem35  42664  stoweidlem60  42689  or2expropbi  43613  ich2exprop  43975
  Copyright terms: Public domain W3C validator