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

Theorem 2eximdv 1634
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 1632 . 2  |-  ( ph  ->  ( E. y ps 
->  E. y ch )
)
32eximdv 1632 1  |-  ( ph  ->  ( E. x E. y ps  ->  E. x E. y ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1550
This theorem is referenced by:  cgsex2g  2988  cgsex4g  2989  spc2egv  3038  spc3egv  3040  relop  5023  elres  5181  opabbrex  6118  th3q  7013  en3  7345  en4  7346  hash2prde  11688  usgrarnedg  21404  fundmpss  25390  pellexlem5  26896  fnchoice  27676  stoweidlem35  27760  stoweidlem60  27785  a9e2eq  28644
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator