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

Theorem 2eximdv 1766
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1706. (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 1764 . 2  |-  ( ph  ->  ( E. y ps 
->  E. y ch )
)
32eximdv 1764 1  |-  ( ph  ->  ( E. x E. y ps  ->  E. x E. y ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758
This theorem depends on definitions:  df-bi 189  df-ex 1664
This theorem is referenced by:  2eu6  2387  cgsex2g  3081  cgsex4g  3082  spc2egv  3136  spc3egv  3138  relop  4985  elres  5140  en3  7808  en4  7809  addsrpr  9499  mulsrpr  9500  hash2prde  12631  pmtrrn2  17101  usgrarnedg  25111  fundmpss  30407  pellexlem5  35677  ax6e2eq  36924  fnchoice  37350  fzisoeu  37518  stoweidlem35  37896  stoweidlem60  37921  umgredg  39229  usgedgimp  39768  usgedgimpALT  39771
  Copyright terms: Public domain W3C validator