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

Theorem 2eximdv 1612
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 1610 . 2  |-  ( ph  ->  ( E. y ps 
->  E. y ch )
)
32eximdv 1610 1  |-  ( ph  ->  ( E. x E. y ps  ->  E. x E. y ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1530
This theorem is referenced by:  cgsex2g  2822  cgsex4g  2823  spc2egv  2872  spc3egv  2874  relop  4836  elres  4992  th3q  6769  en3  7097  en4  7098  fundmpss  24124  ssoprab2g  25043  pellexlem5  26929  fnchoice  27711  stoweidlem35  27795  a9e2eq  28379
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605
This theorem depends on definitions:  df-bi 177  df-ex 1531
  Copyright terms: Public domain W3C validator