Theorem 19.8a 1583

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

Step	Hyp	Ref	Expression
1		id 19	. . 3 ⊢ (∃𝑥𝜑 → ∃𝑥𝜑)
2		hbe1 1488	. . . 4 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
3	2	19.23h 1491	. . 3 ⊢ (∀𝑥(𝜑 → ∃𝑥𝜑) ↔ (∃𝑥𝜑 → ∃𝑥𝜑))
4	1, 3	mpbir 145	. 2 ⊢ ∀𝑥(𝜑 → ∃𝑥𝜑)
5	4	spi 1529	1 ⊢ (𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1346  ∃wex 1485

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 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.8ad  1584  19.23bi  1585  exim  1592  19.43  1621  hbex  1629  19.2  1631  19.9t  1635  19.9h  1636  excomim  1656  19.38  1669  nexr  1685  sbequ1  1761  equs5e  1788  exdistrfor  1793  sbcof2  1803  mo2n  2047  euor2  2077  2moex  2105  2euex  2106  2moswapdc  2109  2exeu  2111  rspe  2519  rsp2e  2521  ceqex  2857  vn0m  3426  intab  3860  copsexg  4229  eusv2nf  4441  dmcosseq  4882  dminss  5025  imainss  5026  relssdmrn  5131  oprabid  5885  tfrlemibxssdm  6306  tfr1onlembxssdm  6322  tfrcllembxssdm  6335  snexxph  6927  nqprl  7513  nqpru  7514  ltsopr  7558  ltexprlemm  7562  recexprlemopl  7587  recexprlemopu  7589  suplocexprlemrl  7679