Theorem 19.8a 1588

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

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

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 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.8ad  1589  19.23bi  1590  exim  1597  19.43  1626  hbex  1634  19.2  1636  19.9t  1640  19.9h  1641  excomim  1661  19.38  1674  nexr  1690  sbequ1  1766  equs5e  1793  exdistrfor  1798  sbcof2  1808  mo2n  2052  euor2  2082  2moex  2110  2euex  2111  2moswapdc  2114  2exeu  2116  rspe  2524  rsp2e  2526  ceqex  2862  vn0m  3432  intab  3869  copsexg  4238  eusv2nf  4450  dmcosseq  4891  dminss  5035  imainss  5036  relssdmrn  5141  oprabid  5897  tfrlemibxssdm  6318  tfr1onlembxssdm  6334  tfrcllembxssdm  6347  snexxph  6939  nqprl  7525  nqpru  7526  ltsopr  7570  ltexprlemm  7574  recexprlemopl  7599  recexprlemopu  7601  suplocexprlemrl  7691