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

Theorem 2eximdv 1615
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 1613 . 2  |-  ( ph  ->  ( E. y ps 
->  E. y ch )
)
32eximdv 1613 1  |-  ( ph  ->  ( E. x E. y ps  ->  E. x E. y ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1532
This theorem is referenced by:  cgsex2g  2854  cgsex4g  2855  spc2egv  2904  spc3egv  2906  relop  4871  elres  5027  th3q  6810  en3  7140  en4  7141  fundmpss  24507  pellexlem5  26066  fnchoice  26848  stoweidlem35  26932  opabbrex  27248  hash2prde  27284  usgrarnedg  27355  a9e2eq  27817
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607
This theorem depends on definitions:  df-bi 177  df-ex 1533
  Copyright terms: Public domain W3C validator