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

Theorem 2eximi 1533
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 1532 . 2  |-  ( E. y ph  ->  E. y ps )
32eximi 1532 1  |-  ( E. x E. y ph  ->  E. x E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-ial 1468
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  excomim  1594  cgsex2g  2636  cgsex4g  2637  vtocl2  2655  vtocl3  2656  dtruarb  3970  opelopabsb  4023  mosubopt  4431  xpmlem  4774  brabvv  5582  ssoprab2i  5624  dmaddpqlem  6629  nqpi  6630  dmaddpq  6631  dmmulpq  6632  enq0sym  6684  enq0ref  6685  enq0tr  6686  nq0nn  6694  prarloc  6755  bj-inex  10856
  Copyright terms: Public domain W3C validator