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

Theorem 2eximi 1563
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 1562 . 2  |-  ( E. y ph  ->  E. y ps )
32eximi 1562 1  |-  ( E. x E. y ph  ->  E. x E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1451
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-ial 1497
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  excomim  1624  cgsex2g  2694  cgsex4g  2695  vtocl2  2713  vtocl3  2714  dtruarb  4083  opelopabsb  4150  mosubopt  4572  xpmlem  4927  brabvv  5783  ssoprab2i  5826  dmaddpqlem  7149  nqpi  7150  dmaddpq  7151  dmmulpq  7152  enq0sym  7204  enq0ref  7205  enq0tr  7206  nq0nn  7214  prarloc  7275  bj-inex  12907
  Copyright terms: Public domain W3C validator