Theorem 19.8a 1601

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

Syntax hints:   → wi 4  ∀wal 1362  ∃wex 1503

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 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.8ad  1602  19.23bi  1603  exim  1610  19.43  1639  hbex  1647  19.2  1649  19.9t  1653  19.9h  1654  excomim  1674  19.38  1687  nexr  1703  sbequ1  1779  equs5e  1806  exdistrfor  1811  sbcof2  1821  mo2n  2070  euor2  2100  2moex  2128  2euex  2129  2moswapdc  2132  2exeu  2134  rspe  2543  rsp2e  2545  ceqex  2887  vn0m  3458  intab  3899  copsexg  4273  eusv2nf  4487  dmcosseq  4933  dminss  5080  imainss  5081  relssdmrn  5186  oprabid  5950  tfrlemibxssdm  6380  tfr1onlembxssdm  6396  tfrcllembxssdm  6409  snexxph  7009  nqprl  7611  nqpru  7612  ltsopr  7656  ltexprlemm  7660  recexprlemopl  7685  recexprlemopu  7687  suplocexprlemrl  7777  divsfval  12911