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

Theorem 2eximi 1474
 Description: Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
Hypothesis
Ref Expression
eximi.1 (φψ)
Assertion
Ref Expression
2eximi (xyφxyψ)

Proof of Theorem 2eximi
StepHypRef Expression
1 eximi.1 . . 3 (φψ)
21eximi 1473 . 2 (yφyψ)
32eximi 1473 1 (xyφxyψ)
 Colors of variables: wff set class Syntax hints:   → wi 4  ∃wex 1362 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-ial 1409 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  excomim  1535  cgsex2g  2567  cgsex4g  2568  vtocl2  2586  vtocl3  2587  dtruarb  3916  opelopabsb  3971  mosubopt  4332  xpmlem  4671  brabvv  5474  ssoprab2i  5516  dmaddpqlem  6236  nqpi  6237  dmaddpq  6238  dmmulpq  6239  enq0sym  6287  enq0ref  6288  enq0tr  6289  nq0nn  6297  prarloc  6357  bj-inex  7130
 Copyright terms: Public domain W3C validator