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

Theorem 2eximdv 1756
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1701. (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 1754 . 2  |-  ( ph  ->  ( E. y ps 
->  E. y ch )
)
32eximdv 1754 1  |-  ( ph  ->  ( E. x E. y ps  ->  E. x E. y ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748
This theorem depends on definitions:  df-bi 188  df-ex 1660
This theorem is referenced by:  2eu6  2356  cgsex2g  3115  cgsex4g  3116  spc2egv  3168  spc3egv  3170  relop  5001  elres  5156  en3  7811  en4  7812  addsrpr  9500  mulsrpr  9501  hash2prde  12629  hash2prv  12640  hash2sspr  12641  pmtrrn2  17089  usgrarnedg  25098  fundmpss  30402  pellexlem5  35597  ax6e2eq  36782  fnchoice  37211  fzisoeu  37360  stoweidlem35  37716  stoweidlem60  37741  usgrrnedg  38917  usgedgimp  38987  usgedgimpALT  38990
  Copyright terms: Public domain W3C validator