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

Theorem 2eximdv 1888
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1801. (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 1886 . 2 (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒))
32eximdv 1886 1 (𝜑 → (∃𝑥𝑦𝜓 → ∃𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-ex 1745
This theorem is referenced by:  2eu6  2587  cgsex2g  3270  cgsex4g  3271  spc2egv  3326  spc3egv  3328  relop  5305  elres  5470  en3  8238  en4  8239  addsrpr  9934  mulsrpr  9935  hash2prde  13290  pmtrrn2  17926  umgredg  26078  umgr2wlkon  26915  fundmpss  31790  pellexlem5  37714  ax6e2eq  39090  fnchoice  39502  fzisoeu  39828  stoweidlem35  40570  stoweidlem60  40595
  Copyright terms: Public domain W3C validator