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

Theorem 2eximdv 1717
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1659. (Contributed by NM, 3-Aug-1995.)
Hypothesis
Ref Expression
2alimdv.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
2eximdv  |-  ( ph  ->  ( E. x E. y ps  ->  E. x E. y ch ) )
Distinct variable groups:    ph, x    ph, y
Allowed substitution hints:    ps( x, y)    ch( x, y)

Proof of Theorem 2eximdv
StepHypRef Expression
1 2alimdv.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21eximdv 1715 . 2  |-  ( ph  ->  ( E. y ps 
->  E. y ch )
)
32eximdv 1715 1  |-  ( ph  ->  ( E. x E. y ps  ->  E. x E. y ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709
This theorem depends on definitions:  df-bi 185  df-ex 1618
This theorem is referenced by:  2eu6  2380  cgsex2g  3140  cgsex4g  3141  spc2egv  3193  spc3egv  3195  relop  5142  elres  5297  en3  7749  en4  7750  addsrpr  9441  mulsrpr  9442  hash2prde  12503  hash2prv  12512  hash2sspr  12513  pmtrrn2  16687  usgrarnedg  24589  fundmpss  29440  pellexlem5  31011  fnchoice  31647  fzisoeu  31742  stoweidlem35  32059  stoweidlem60  32084  usgedgimp  32794  usgedgimpALT  32797  ax6e2eq  33743
  Copyright terms: Public domain W3C validator