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

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

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