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

Theorem 2eximi 1601
Description: Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
Hypothesis
Ref Expression
eximi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
2eximi  |-  ( E. x E. y ph  ->  E. x E. y ps )

Proof of Theorem 2eximi
StepHypRef Expression
1 eximi.1 . . 3  |-  ( ph  ->  ps )
21eximi 1600 . 2  |-  ( E. y ph  ->  E. y ps )
32eximi 1600 1  |-  ( E. x E. y ph  ->  E. x E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1492
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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  excomim  1663  cgsex2g  2773  cgsex4g  2774  vtocl2  2792  vtocl3  2793  dtruarb  4191  opelopabsb  4260  mosubopt  4691  xpmlem  5049  brabvv  5920  ssoprab2i  5963  dmaddpqlem  7375  nqpi  7376  dmaddpq  7377  dmmulpq  7378  enq0sym  7430  enq0ref  7431  enq0tr  7432  nq0nn  7440  prarloc  7501  bj-inex  14629
  Copyright terms: Public domain W3C validator