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  2866  vn0m  3436  intab  3875  copsexg  4246  eusv2nf  4458  dmcosseq  4900  dminss  5045  imainss  5046  relssdmrn  5151  oprabid  5909  tfrlemibxssdm  6330  tfr1onlembxssdm  6346  tfrcllembxssdm  6359  snexxph  6951  nqprl  7552  nqpru  7553  ltsopr  7597  ltexprlemm  7601  recexprlemopl  7626  recexprlemopu  7628  suplocexprlemrl  7718