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

Theorem 2eximdv 1679
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 1677 . 2  |-  ( ph  ->  ( E. y ps 
->  E. y ch )
)
32eximdv 1677 1  |-  ( ph  ->  ( E. x E. y ps  ->  E. x E. y ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671
This theorem depends on definitions:  df-bi 185  df-ex 1588
This theorem is referenced by:  2eu6  2380  cgsex2g  3112  cgsex4g  3113  spc2egv  3165  spc3egv  3167  relop  5099  elres  5254  th3q  7320  en3  7661  en4  7662  hash2prde  12298  pmtrrn2  16086  usgrarnedg  23456  fundmpss  27722  pellexlem5  29323  fnchoice  29900  stoweidlem35  29979  stoweidlem60  30004  hash2prv  30375  hash2sspr  30376  ax6e2eq  31599
  Copyright terms: Public domain W3C validator