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

Theorem eximi 1562
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 1561 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2 eximi.1 . 2 (𝜑𝜓)
31, 2mpg 1410 1 (∃𝑥𝜑 → ∃𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1451
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-ial 1497
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  2eximi  1563  eximii  1564  exsimpl  1579  exsimpr  1580  19.29r2  1584  19.29x  1585  19.35-1  1586  19.43  1590  19.40  1593  19.40-2  1594  exanaliim  1609  19.12  1626  equs4  1686  cbvexh  1711  equvini  1714  sbimi  1720  equs5e  1749  exdistrfor  1754  equs45f  1756  sbcof2  1764  sbequi  1793  spsbe  1796  sbidm  1805  cbvexdh  1876  eumo0  2006  mor  2017  euan  2031  eupickb  2056  2eu2ex  2064  2exeu  2067  rexex  2454  reximi2  2503  cgsexg  2693  gencbvex  2704  gencbval  2706  vtocl3  2714  eqvinc  2780  eqvincg  2781  mosubt  2832  rexm  3430  prmg  3612  bm1.3ii  4017  a9evsep  4018  axnul  4021  dminss  4921  imainss  4922  euiotaex  5072  imadiflem  5170  funimaexglem  5174  brprcneu  5380  fv3  5410  relelfvdm  5419  ssimaex  5448  oprabid  5769  brabvv  5783  ecexr  6400  enssdom  6622  fidcenumlemim  6806  subhalfnqq  7186  prarloc  7275  ltexprlemopl  7373  ltexprlemlol  7374  ltexprlemopu  7375  ltexprlemupu  7376  bdbm1.3ii  12891  bj-inex  12907  bj-2inf  12938
  Copyright terms: Public domain W3C validator