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

Theorem 2eximi 1581
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 1580 . 2  |-  ( E. y ph  ->  E. y ps )
32eximi 1580 1  |-  ( E. x E. y ph  ->  E. x E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1472
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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-ial 1514
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  excomim  1643  cgsex2g  2748  cgsex4g  2749  vtocl2  2767  vtocl3  2768  dtruarb  4152  opelopabsb  4220  mosubopt  4651  xpmlem  5006  brabvv  5867  ssoprab2i  5910  dmaddpqlem  7297  nqpi  7298  dmaddpq  7299  dmmulpq  7300  enq0sym  7352  enq0ref  7353  enq0tr  7354  nq0nn  7362  prarloc  7423  bj-inex  13493
  Copyright terms: Public domain W3C validator