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 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 1918 . 2 (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒))
32eximdv 1918 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 1911
This theorem depends on definitions:  df-bi 206  df-ex 1780
This theorem is referenced by:  2eu6  2650  cgsex2g  3518  cgsex4g  3519  cgsex4gOLD  3520  cgsex4gOLDOLD  3521  spc2egv  3588  rexopabb  5527  relop  5849  elinxp  6018  opreuopreu  8022  en3  9284  en4  9285  addsrpr  11072  mulsrpr  11073  hash2prde  14435  pmtrrn2  19369  umgredg  28665  umgr2wlkon  29471  trsp2cyc  32552  acycgrsubgr  34447  satfvsucsuc  34654  fmla0xp  34672  fundmpss  35042  pellexlem5  41873  ax6e2eq  43620  fnchoice  44015  fzisoeu  44308  stoweidlem35  45049  stoweidlem60  45074  or2expropbi  46042  ich2exprop  46437
  Copyright terms: Public domain W3C validator