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

Theorem 19.8a 1525
Description: If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
19.8a (𝜑 → ∃𝑥𝜑)

Proof of Theorem 19.8a
StepHypRef Expression
1 id 19 . . 3 (∃𝑥𝜑 → ∃𝑥𝜑)
2 hbe1 1427 . . . 4 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
3219.23h 1430 . . 3 (∀𝑥(𝜑 → ∃𝑥𝜑) ↔ (∃𝑥𝜑 → ∃𝑥𝜑))
41, 3mpbir 144 . 2 𝑥(𝜑 → ∃𝑥𝜑)
54spi 1472 1 (𝜑 → ∃𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1285  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-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  19.23bi  1526  exim  1533  19.43  1562  hbex  1570  19.2  1572  19.9t  1576  19.9h  1577  excomim  1596  19.38  1609  nexr  1625  sbequ1  1695  equs5e  1720  exdistrfor  1725  sbcof2  1735  mo2n  1973  euor2  2003  2moex  2031  2euex  2032  2moswapdc  2035  2exeu  2037  rspe  2420  rsp2e  2422  ceqex  2735  vn0m  3283  intab  3700  copsexg  4045  eusv2nf  4252  dmcosseq  4672  dminss  4812  imainss  4813  relssdmrn  4917  oprabid  5638  tfrlemibxssdm  6046  tfr1onlembxssdm  6062  tfrcllembxssdm  6075  snexxph  6608  nqprl  7054  nqpru  7055  ltsopr  7099  ltexprlemm  7103  recexprlemopl  7128  recexprlemopu  7130
  Copyright terms: Public domain W3C validator