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

Theorem 19.8a 1498
 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 1400 . . . 4 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
3219.23h 1403 . . 3 (∀𝑥(𝜑 → ∃𝑥𝜑) ↔ (∃𝑥𝜑 → ∃𝑥𝜑))
41, 3mpbir 138 . 2 𝑥(𝜑 → ∃𝑥𝜑)
54spi 1445 1 (𝜑 → ∃𝑥𝜑)
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1257  ∃wex 1397 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  19.23bi  1499  exim  1506  19.43  1535  hbex  1543  19.2  1545  19.9t  1549  19.9h  1550  excomim  1569  19.38  1582  nexr  1598  sbequ1  1667  equs5e  1692  exdistrfor  1697  sbcof2  1707  mo2n  1944  euor2  1974  2moex  2002  2euex  2003  2moswapdc  2006  2exeu  2008  rspe  2387  rsp2e  2389  ceqex  2694  vn0m  3260  intab  3672  copsexg  4009  eusv2nf  4216  dmcosseq  4631  dminss  4766  imainss  4767  relssdmrn  4869  oprabid  5565  tfrlemibxssdm  5972  nqprl  6707  nqpru  6708  ltsopr  6752  ltexprlemm  6756  recexprlemopl  6781  recexprlemopu  6783
 Copyright terms: Public domain W3C validator