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

Theorem rexlimivv 2494
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.)
Hypothesis
Ref Expression
rexlimivv.1  |-  ( ( x  e.  A  /\  y  e.  B )  ->  ( ph  ->  ps ) )
Assertion
Ref Expression
rexlimivv  |-  ( E. x  e.  A  E. y  e.  B  ph  ->  ps )
Distinct variable groups:    x, y, ps    y, A
Allowed substitution hints:    ph( x, y)    A( x)    B( x, y)

Proof of Theorem rexlimivv
StepHypRef Expression
1 rexlimivv.1 . . 3  |-  ( ( x  e.  A  /\  y  e.  B )  ->  ( ph  ->  ps ) )
21rexlimdva 2489 . 2  |-  ( x  e.  A  ->  ( E. y  e.  B  ph 
->  ps ) )
32rexlimiv 2483 1  |-  ( E. x  e.  A  E. y  e.  B  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    e. wcel 1438   E.wrex 2360
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-i5r 1473
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-ral 2364  df-rex 2365
This theorem is referenced by:  opelxp  4467  f1o2ndf1  5993  xpdom2  6547  distrlem5prl  7145  distrlem5pru  7146  mulid1  7485  cnegex  7660  recexap  8122  creur  8419  creui  8420  cju  8421  elz2  8818  qre  9110  qaddcl  9120  qnegcl  9121  qmulcl  9122  qreccl  9127  replim  10293  odd2np1  11151  opoe  11173  omoe  11174  opeo  11175  omeo  11176  qredeu  11357
  Copyright terms: Public domain W3C validator