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

Theorem eximi 1534
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 1533 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2 eximi.1 . 2 (𝜑𝜓)
31, 2mpg 1383 1 (∃𝑥𝜑 → ∃𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  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  3935  a9evsep  3936  axnul  3939  dminss  4812  imainss  4813  euiotaex  4962  imadiflem  5058  funimaexglem  5062  brprcneu  5261  fv3  5291  relelfvdm  5299  ssimaex  5328  oprabid  5638  brabvv  5652  ecexr  6249  enssdom  6431  subhalfnqq  6917  prarloc  7006  ltexprlemopl  7104  ltexprlemlol  7105  ltexprlemopu  7106  ltexprlemupu  7107  bdbm1.3ii  11220  bj-inex  11236  bj-2inf  11271
  Copyright terms: Public domain W3C validator