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

Theorem 2eximi 1580
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 1579 . 2  |-  ( E. y ph  ->  E. y ps )
32eximi 1579 1  |-  ( E. x E. y ph  ->  E. x E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1468
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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-ial 1514
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  excomim  1641  cgsex2g  2722  cgsex4g  2723  vtocl2  2741  vtocl3  2742  dtruarb  4115  opelopabsb  4182  mosubopt  4604  xpmlem  4959  brabvv  5817  ssoprab2i  5860  dmaddpqlem  7185  nqpi  7186  dmaddpq  7187  dmmulpq  7188  enq0sym  7240  enq0ref  7241  enq0tr  7242  nq0nn  7250  prarloc  7311  bj-inex  13105
  Copyright terms: Public domain W3C validator