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

Theorem eximi 1507
Description: Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eximi.1 (𝜑𝜓)
Assertion
Ref Expression
eximi (∃𝑥𝜑 → ∃𝑥𝜓)

Proof of Theorem eximi
StepHypRef Expression
1 exim 1506 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2 eximi.1 . 2 (𝜑𝜓)
31, 2mpg 1356 1 (∃𝑥𝜑 → ∃𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1397
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-ial 1443
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  2eximi  1508  eximii  1509  exsimpl  1524  exsimpr  1525  19.29r2  1529  19.29x  1530  19.35-1  1531  19.43  1535  19.40  1538  19.40-2  1539  exanaliim  1554  19.12  1571  equs4  1629  cbvexh  1654  equvini  1657  sbimi  1663  equs5e  1692  exdistrfor  1697  equs45f  1699  sbcof2  1707  sbequi  1736  spsbe  1739  sbidm  1747  cbvexdh  1817  eumo0  1947  mor  1958  euan  1972  eupickb  1997  2eu2ex  2005  2exeu  2008  rexex  2385  reximi2  2432  cgsexg  2606  gencbvex  2617  gencbval  2619  vtocl3  2627  eqvinc  2690  eqvincg  2691  mosubt  2741  rexm  3348  prmg  3517  bm1.3ii  3906  a9evsep  3907  axnul  3910  dtruex  4311  dminss  4766  imainss  4767  euiotaex  4911  imadiflem  5006  funimaexglem  5010  brprcneu  5199  fv3  5225  relelfvdm  5233  ssimaex  5262  oprabid  5565  brabvv  5579  ecexr  6142  enssdom  6273  subhalfnqq  6570  prarloc  6659  ltexprlemopl  6757  ltexprlemlol  6758  ltexprlemopu  6759  ltexprlemupu  6760  bdbm1.3ii  10398  bj-inex  10414  bj-2inf  10449
  Copyright terms: Public domain W3C validator