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

Theorem rexlimdvva 2457
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 112 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ( ps  ->  ch ) ) )
32rexlimdvv 2456 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    e. wcel 1409   E.wrex 2324
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-i5r 1444
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-ral 2328  df-rex 2329
This theorem is referenced by:  ovelrn  5677  f1o2ndf1  5877  eroveu  6228  eroprf  6230  genipv  6665  genpelvl  6668  genpelvu  6669  genprndl  6677  genprndu  6678  addlocpr  6692  addnqprlemrl  6713  addnqprlemru  6714  mulnqprlemrl  6729  mulnqprlemru  6730  ltsopr  6752  ltaddpr  6753  ltexprlemfl  6765  ltexprlemrl  6766  ltexprlemfu  6767  ltexprlemru  6768  cauappcvgprlemladdfu  6810  cauappcvgprlemladdfl  6811  caucvgprlemdisj  6830  caucvgprlemladdfu  6833  caucvgprprlemdisj  6858  apreap  7652  apreim  7668  apirr  7670  apsym  7671  apcotr  7672  apadd1  7673  apneg  7676  mulext1  7677  apti  7687  qapne  8671  qtri3or  9200  qbtwnzlemex  9207  rebtwn2z  9211  cjap  9734  climcn2  10061  dvds2lem  10120
  Copyright terms: Public domain W3C validator