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  2066  euor2  2096  2moex  2124  2euex  2125  2moswapdc  2128  2exeu  2130  rspe  2539  rsp2e  2541  ceqex  2879  vn0m  3449  intab  3891  copsexg  4265  eusv2nf  4477  dmcosseq  4919  dminss  5064  imainss  5065  relssdmrn  5170  oprabid  5932  tfrlemibxssdm  6356  tfr1onlembxssdm  6372  tfrcllembxssdm  6385  snexxph  6983  nqprl  7585  nqpru  7586  ltsopr  7630  ltexprlemm  7634  recexprlemopl  7659  recexprlemopu  7661  suplocexprlemrl  7751