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

Theorem 2eximi 1594
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 1593 . 2  |-  ( E. y ph  ->  E. y ps )
32eximi 1593 1  |-  ( E. x E. y ph  ->  E. x E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1485
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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-ial 1527
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  excomim  1656  cgsex2g  2766  cgsex4g  2767  vtocl2  2785  vtocl3  2786  dtruarb  4177  opelopabsb  4245  mosubopt  4676  xpmlem  5031  brabvv  5899  ssoprab2i  5942  dmaddpqlem  7339  nqpi  7340  dmaddpq  7341  dmmulpq  7342  enq0sym  7394  enq0ref  7395  enq0tr  7396  nq0nn  7404  prarloc  7465  bj-inex  13942
  Copyright terms: Public domain W3C validator