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

Theorem 19.8a 1601
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 1506 . . . 4 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
3219.23h 1509 . . 3 (∀𝑥(𝜑 → ∃𝑥𝜑) ↔ (∃𝑥𝜑 → ∃𝑥𝜑))
41, 3mpbir 146 . 2 𝑥(𝜑 → ∃𝑥𝜑)
54spi 1547 1 (𝜑 → ∃𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1362  wex 1503
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  19.8ad  1602  19.23bi  1603  exim  1610  19.43  1639  hbex  1647  19.2  1649  19.9t  1653  19.9h  1654  excomim  1674  19.38  1687  nexr  1703  sbequ1  1779  equs5e  1806  exdistrfor  1811  sbcof2  1821  mo2n  2066  euor2  2096  2moex  2124  2euex  2125  2moswapdc  2128  2exeu  2130  rspe  2539  rsp2e  2541  ceqex  2879  vn0m  3449  intab  3891  copsexg  4265  eusv2nf  4477  dmcosseq  4919  dminss  5064  imainss  5065  relssdmrn  5170  oprabid  5932  tfrlemibxssdm  6356  tfr1onlembxssdm  6372  tfrcllembxssdm  6385  snexxph  6983  nqprl  7585  nqpru  7586  ltsopr  7630  ltexprlemm  7634  recexprlemopl  7659  recexprlemopu  7661  suplocexprlemrl  7751
  Copyright terms: Public domain W3C validator