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

Theorem rexlimdvva 2600
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
rexlimdvva.1  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( ps  ->  ch ) )
Assertion
Ref Expression
rexlimdvva  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Distinct variable groups:    x, y, ph    ch, x, y    y, A
Allowed substitution hints:    ps( x, y)    A( x)    B( x, y)

Proof of Theorem rexlimdvva
StepHypRef Expression
1 rexlimdvva.1 . . 3  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( ps  ->  ch ) )
21ex 115 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ( ps  ->  ch ) ) )
32rexlimdvv 2599 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    e. wcel 2146   E.wrex 2454
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-17 1524  ax-ial 1532  ax-i5r 1533
This theorem depends on definitions:  df-bi 117  df-nf 1459  df-ral 2458  df-rex 2459
This theorem is referenced by:  ovelrn  6013  f1o2ndf1  6219  eroveu  6616  eroprf  6618  genipv  7483  genpelvl  7486  genpelvu  7487  genprndl  7495  genprndu  7496  addlocpr  7510  addnqprlemrl  7531  addnqprlemru  7532  mulnqprlemrl  7547  mulnqprlemru  7548  ltsopr  7570  ltaddpr  7571  ltexprlemfl  7583  ltexprlemrl  7584  ltexprlemfu  7585  ltexprlemru  7586  cauappcvgprlemladdfu  7628  cauappcvgprlemladdfl  7629  caucvgprlemdisj  7648  caucvgprlemladdfu  7651  caucvgprprlemdisj  7676  apreap  8518  apreim  8534  apirr  8536  apsym  8537  apcotr  8538  apadd1  8539  apneg  8542  mulext1  8543  apti  8553  aprcl  8577  qapne  9610  qtri3or  10211  exbtwnzlemex  10218  rebtwn2z  10223  cjap  10882  rexanre  11196  climcn2  11284  summodc  11358  prodmodclem2  11552  prodmodc  11553  eirrap  11752  dvds2lem  11777  bezoutlemnewy  11963  bezoutlembi  11972  dvdsmulgcd  11992  divgcdcoprm0  12067  cncongr1  12069  sqrt2irrap  12146  pcqmul  12269  pcneg  12290  pcadd  12305  4sqlem1  12352  4sqlem2  12353  4sqlem4  12356  mul4sq  12358  restbasg  13161  txbas  13251  blin2  13425  xmettxlem  13502  xmettx  13503  addcncntoplem  13544  mulcncf  13584  logbgcd1irr  13878  logbgcd1irrap  13881  2sqlem5  13948  2sqlem9  13953
  Copyright terms: Public domain W3C validator