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  2888  vn0m  3459  intab  3900  copsexg  4274  eusv2nf  4488  dmcosseq  4934  dminss  5081  imainss  5082  relssdmrn  5187  oprabid  5951  tfrlemibxssdm  6382  tfr1onlembxssdm  6398  tfrcllembxssdm  6411  snexxph  7011  nqprl  7613  nqpru  7614  ltsopr  7658  ltexprlemm  7662  recexprlemopl  7687  recexprlemopu  7689  suplocexprlemrl  7779  divsfval  12914