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

Theorem 19.8a 1552
Description: If a wff is true, then 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 1454 . . . 4 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
3219.23h 1457 . . 3 (∀𝑥(𝜑 → ∃𝑥𝜑) ↔ (∃𝑥𝜑 → ∃𝑥𝜑))
41, 3mpbir 145 . 2 𝑥(𝜑 → ∃𝑥𝜑)
54spi 1499 1 (𝜑 → ∃𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1312  wex 1451
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  19.8ad  1553  19.23bi  1554  exim  1561  19.43  1590  hbex  1598  19.2  1600  19.9t  1604  19.9h  1605  excomim  1624  19.38  1637  nexr  1653  sbequ1  1724  equs5e  1749  exdistrfor  1754  sbcof2  1764  mo2n  2003  euor2  2033  2moex  2061  2euex  2062  2moswapdc  2065  2exeu  2067  rspe  2455  rsp2e  2457  ceqex  2782  vn0m  3340  intab  3766  copsexg  4126  eusv2nf  4337  dmcosseq  4768  dminss  4911  imainss  4912  relssdmrn  5017  oprabid  5757  tfrlemibxssdm  6178  tfr1onlembxssdm  6194  tfrcllembxssdm  6207  snexxph  6790  nqprl  7307  nqpru  7308  ltsopr  7352  ltexprlemm  7356  recexprlemopl  7381  recexprlemopu  7383
  Copyright terms: Public domain W3C validator