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

Theorem rexlimivv 2580
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 2574 . 2  |-  ( x  e.  A  ->  ( E. y  e.  B  ph 
->  ps ) )
32rexlimiv 2568 1  |-  ( E. x  e.  A  E. y  e.  B  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    e. wcel 2128   E.wrex 2436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-i5r 1515
This theorem depends on definitions:  df-bi 116  df-nf 1441  df-ral 2440  df-rex 2441
This theorem is referenced by:  opelxp  4617  f1o2ndf1  6176  xpdom2  6777  distrlem5prl  7507  distrlem5pru  7508  mulid1  7876  cnegex  8054  recexap  8528  creur  8831  creui  8832  cju  8833  elz2  9236  qre  9535  qaddcl  9545  qnegcl  9546  qmulcl  9547  qreccl  9552  elpqb  9559  replim  10763  prodmodc  11479  odd2np1  11768  opoe  11790  omoe  11791  opeo  11792  omeo  11793  qredeu  11978  pythagtriplem1  12144  txuni2  12698  blssioo  12987  tgioo  12988
  Copyright terms: Public domain W3C validator