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

Theorem eximi 1469
Description: Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eximi.1 (φψ)
Assertion
Ref Expression
eximi (xφxψ)

Proof of Theorem eximi
StepHypRef Expression
1 exim 1468 . 2 (x(φψ) → (xφxψ))
2 eximi.1 . 2 (φψ)
31, 2mpg 1316 1 (xφxψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1358
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 1312  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-4 1377  ax-ial 1405
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  2eximi  1470  eximii  1471  exsimpl  1486  exsimpr  1487  19.29r2  1491  19.29x  1492  19.35-1  1493  19.43  1497  19.40  1500  19.40-2  1501  exanaliim  1516  19.12  1533  equs4  1591  cbvexh  1616  equvini  1619  sbimi  1625  equs5e  1654  exdistrfor  1659  equs45f  1661  sbcof2  1669  sbequi  1698  spsbe  1701  sbidm  1709  cbvexdh  1779  eumo0  1909  mor  1920  euan  1934  eupickb  1959  2eu2ex  1967  2exeu  1970  rexex  2342  reximi2  2389  cgsexg  2562  gencbvex  2573  gencbval  2575  vtocl3  2583  eqvinc  2640  eqvincg  2641  mosubt  2691  rexm  3295  prmg  3459  bm1.3ii  3848  a9evsep  3849  axnul  3852  dtruex  4217  dminss  4661  imainss  4662  euiotaex  4806  imadiflem  4900  funimaexglem  4904  brprcneu  5092  fv3  5118  relelfvdm  5126  ssimaex  5155  oprabid  5457  brabvv  5470  ecexr  6018  subhalfnqq  6265  prarloc  6351  ltexprlemopl  6432  ltexprlemlol  6433  ltexprlemopu  6434  ltexprlemupu  6435  bdbm1.3ii  7256  bj-inex  7269  bj-2inf  7299
  Copyright terms: Public domain W3C validator