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

Theorem 2eximdv 1610
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (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 1608 . 2  |-  ( ph  ->  ( E. y ps 
->  E. y ch )
)
32eximdv 1608 1  |-  ( ph  ->  ( E. x E. y ps  ->  E. x E. y ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1528
This theorem is referenced by:  cgsex2g  2820  cgsex4g  2821  spc2egv  2870  spc3egv  2872  relop  4834  elres  4990  th3q  6767  en3  7095  en4  7096  fundmpss  24122  ssoprab2g  25032  pellexlem5  26918  fnchoice  27700  stoweidlem35  27784  a9e2eq  28323
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603
This theorem depends on definitions:  df-bi 177  df-ex 1529
  Copyright terms: Public domain W3C validator