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

Theorem 2eximdv 1635
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 1633 . 2  |-  ( ph  ->  ( E. y ps 
->  E. y ch )
)
32eximdv 1633 1  |-  ( ph  ->  ( E. x E. y ps  ->  E. x E. y ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1551
This theorem is referenced by:  cgsex2g  2990  cgsex4g  2991  spc2egv  3040  spc3egv  3042  relop  5026  elres  5184  opabbrex  6121  th3q  7016  en3  7348  en4  7349  hash2prde  11693  usgrarnedg  21409  fundmpss  25395  pellexlem5  26910  fnchoice  27690  stoweidlem35  27774  stoweidlem60  27799  hash2prv  28193  hash2sspr  28194  a9e2eq  28718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator