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

Theorem eximi 1534
Description: Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eximi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
eximi  |-  ( E. x ph  ->  E. x ps )

Proof of Theorem eximi
StepHypRef Expression
1 exim 1533 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
2 eximi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1383 1  |-  ( E. x ph  ->  E. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1424
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 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-ial 1470
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  2eximi  1535  eximii  1536  exsimpl  1551  exsimpr  1552  19.29r2  1556  19.29x  1557  19.35-1  1558  19.43  1562  19.40  1565  19.40-2  1566  exanaliim  1581  19.12  1598  equs4  1657  cbvexh  1682  equvini  1685  sbimi  1691  equs5e  1720  exdistrfor  1725  equs45f  1727  sbcof2  1735  sbequi  1764  spsbe  1767  sbidm  1776  cbvexdh  1846  eumo0  1976  mor  1987  euan  2001  eupickb  2026  2eu2ex  2034  2exeu  2037  rexex  2418  reximi2  2465  cgsexg  2648  gencbvex  2659  gencbval  2661  vtocl3  2669  eqvinc  2731  eqvincg  2732  mosubt  2783  rexm  3368  prmg  3544  bm1.3ii  3934  a9evsep  3935  axnul  3938  dminss  4809  imainss  4810  euiotaex  4959  imadiflem  5055  funimaexglem  5059  brprcneu  5255  fv3  5285  relelfvdm  5293  ssimaex  5322  oprabid  5632  brabvv  5646  ecexr  6243  enssdom  6425  subhalfnqq  6910  prarloc  6999  ltexprlemopl  7097  ltexprlemlol  7098  ltexprlemopu  7099  ltexprlemupu  7100  bdbm1.3ii  11212  bj-inex  11228  bj-2inf  11263
  Copyright terms: Public domain W3C validator