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

Theorem 2eximdv 1923
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1837. (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 1921 . 2 (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒))
32eximdv 1921 1 (𝜑 → (∃𝑥𝑦𝜓 → ∃𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-ex 1783
This theorem is referenced by:  2eu6  2657  cgsex2g  3492  cgsex4g  3493  cgsex4gOLD  3494  spc2egv  3561  rexopabb  5490  relop  5811  elinxp  5980  opreuopreu  7971  en3  9233  en4  9234  addsrpr  11018  mulsrpr  11019  hash2prde  14376  pmtrrn2  19249  umgredg  28131  umgr2wlkon  28937  trsp2cyc  32014  acycgrsubgr  33792  satfvsucsuc  33999  fmla0xp  34017  fundmpss  34380  pellexlem5  41185  ax6e2eq  42913  fnchoice  43308  fzisoeu  43608  stoweidlem35  44350  stoweidlem60  44375  or2expropbi  45342  ich2exprop  45737
  Copyright terms: Public domain W3C validator