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

Theorem 2eximdv 1774
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1714. (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 1772 . 2  |-  ( ph  ->  ( E. y ps 
->  E. y ch )
)
32eximdv 1772 1  |-  ( ph  ->  ( E. x E. y ps  ->  E. x E. y ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766
This theorem depends on definitions:  df-bi 190  df-ex 1672
This theorem is referenced by:  2eu6  2407  cgsex2g  3067  cgsex4g  3068  spc2egv  3122  spc3egv  3124  relop  4990  elres  5146  en3  7826  en4  7827  addsrpr  9517  mulsrpr  9518  hash2prde  12672  pmtrrn2  17179  usgrarnedg  25190  fundmpss  30478  pellexlem5  35748  ax6e2eq  36994  fnchoice  37413  fzisoeu  37606  stoweidlem35  38008  stoweidlem60  38033  umgredg  39390  umgr2wlkon  40072  usgedgimp  40223  usgedgimpALT  40226
  Copyright terms: Public domain W3C validator