Theorem 19.8a 1590

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 1495	. . . 4 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
3	2	19.23h 1498	. . 3 ⊢ (∀𝑥(𝜑 → ∃𝑥𝜑) ↔ (∃𝑥𝜑 → ∃𝑥𝜑))
4	1, 3	mpbir 146	. 2 ⊢ ∀𝑥(𝜑 → ∃𝑥𝜑)
5	4	spi 1536	1 ⊢ (𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1351  ∃wex 1492

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 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.8ad  1591  19.23bi  1592  exim  1599  19.43  1628  hbex  1636  19.2  1638  19.9t  1642  19.9h  1643  excomim  1663  19.38  1676  nexr  1692  sbequ1  1768  equs5e  1795  exdistrfor  1800  sbcof2  1810  mo2n  2054  euor2  2084  2moex  2112  2euex  2113  2moswapdc  2116  2exeu  2118  rspe  2526  rsp2e  2528  ceqex  2864  vn0m  3434  intab  3873  copsexg  4244  eusv2nf  4456  dmcosseq  4898  dminss  5043  imainss  5044  relssdmrn  5149  oprabid  5906  tfrlemibxssdm  6327  tfr1onlembxssdm  6343  tfrcllembxssdm  6356  snexxph  6948  nqprl  7549  nqpru  7550  ltsopr  7594  ltexprlemm  7598  recexprlemopl  7623  recexprlemopu  7625  suplocexprlemrl  7715