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

Theorem eximi 1488
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 1487 . 2 (x(φψ) → (xφxψ))
2 eximi.1 . 2 (φψ)
31, 2mpg 1337 1 (xφxψ)
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:  2eximi  1489  eximii  1490  exsimpl  1505  exsimpr  1506  19.29r2  1510  19.29x  1511  19.35-1  1512  19.43  1516  19.40  1519  19.40-2  1520  exanaliim  1535  19.12  1552  equs4  1610  cbvexh  1635  equvini  1638  sbimi  1644  equs5e  1673  exdistrfor  1678  equs45f  1680  sbcof2  1688  sbequi  1717  spsbe  1720  sbidm  1728  cbvexdh  1798  eumo0  1928  mor  1939  euan  1953  eupickb  1978  2eu2ex  1986  2exeu  1989  rexex  2362  reximi2  2409  cgsexg  2583  gencbvex  2594  gencbval  2596  vtocl3  2604  eqvinc  2661  eqvincg  2662  mosubt  2712  rexm  3314  prmg  3480  bm1.3ii  3869  a9evsep  3870  axnul  3873  dtruex  4237  dminss  4681  imainss  4682  euiotaex  4826  imadiflem  4921  funimaexglem  4925  brprcneu  5114  fv3  5140  relelfvdm  5148  ssimaex  5177  oprabid  5480  brabvv  5493  ecexr  6047  enssdom  6178  subhalfnqq  6397  prarloc  6485  ltexprlemopl  6574  ltexprlemlol  6575  ltexprlemopu  6576  ltexprlemupu  6577  bdbm1.3ii  9325  bj-inex  9338  bj-2inf  9372
  Copyright terms: Public domain W3C validator