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

Theorem 19.8a 1570
 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 1472 . . . 4 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
3219.23h 1475 . . 3 (∀𝑥(𝜑 → ∃𝑥𝜑) ↔ (∃𝑥𝜑 → ∃𝑥𝜑))
41, 3mpbir 145 . 2 𝑥(𝜑 → ∃𝑥𝜑)
54spi 1517 1 (𝜑 → ∃𝑥𝜑)
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1330  ∃wex 1469 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  19.8ad  1571  19.23bi  1572  exim  1579  19.43  1608  hbex  1616  19.2  1618  19.9t  1622  19.9h  1623  excomim  1642  19.38  1655  nexr  1671  sbequ1  1742  equs5e  1768  exdistrfor  1773  sbcof2  1783  mo2n  2028  euor2  2058  2moex  2086  2euex  2087  2moswapdc  2090  2exeu  2092  rspe  2484  rsp2e  2486  ceqex  2815  vn0m  3378  intab  3807  copsexg  4173  eusv2nf  4384  dmcosseq  4817  dminss  4960  imainss  4961  relssdmrn  5066  oprabid  5810  tfrlemibxssdm  6231  tfr1onlembxssdm  6247  tfrcllembxssdm  6260  snexxph  6845  nqprl  7382  nqpru  7383  ltsopr  7427  ltexprlemm  7431  recexprlemopl  7456  recexprlemopu  7458  suplocexprlemrl  7548
 Copyright terms: Public domain W3C validator