ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exlimdvv Unicode version

Theorem exlimdvv 1869
Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)
Hypothesis
Ref Expression
exlimdvv.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
exlimdvv  |-  ( ph  ->  ( E. x E. y ps  ->  ch )
)
Distinct variable groups:    ch, x    ph, x    ch, y    ph, y
Allowed substitution hints:    ps( x, y)

Proof of Theorem exlimdvv
StepHypRef Expression
1 exlimdvv.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21exlimdv 1791 . 2  |-  ( ph  ->  ( E. y ps 
->  ch ) )
32exlimdv 1791 1  |-  ( ph  ->  ( E. x E. y ps  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1423  ax-gen 1425  ax-ie2 1470  ax-17 1506
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  euotd  4176  funopg  5157  th3qlem1  6531  fundmen  6700  sbthlemi10  6854  addnq0mo  7267  mulnq0mo  7268  genprndl  7341  genprndu  7342  genpdisj  7343  mullocpr  7391  addsrmo  7563  mulsrmo  7564  cnm  7652  summodc  11164  fsum2dlemstep  11215  prodmodc  11359  txbasval  12450
  Copyright terms: Public domain W3C validator