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

Theorem 2eximi 1489
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 1488 . 2 (yφyψ)
32eximi 1488 1 (xyφxyψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1378
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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-ial 1424
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  excomim  1550  cgsex2g  2584  cgsex4g  2585  vtocl2  2603  vtocl3  2604  dtruarb  3933  opelopabsb  3988  mosubopt  4348  xpmlem  4687  brabvv  5493  ssoprab2i  5535  dmaddpqlem  6361  nqpi  6362  dmaddpq  6363  dmmulpq  6364  enq0sym  6415  enq0ref  6416  enq0tr  6417  nq0nn  6425  prarloc  6486  bj-inex  9362
  Copyright terms: Public domain W3C validator