Theorem 19.8a 1639

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

Syntax hints:   → wi 4  ∀wal 1396  ∃wex 1541

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 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.8ad  1640  19.23bi  1641  exim  1648  19.43  1677  hbex  1685  19.2  1687  19.9t  1691  19.9h  1692  excomim  1711  19.38  1724  nexr  1740  sbequ1  1816  equs5e  1843  exdistrfor  1848  sbcof2  1858  mo2n  2107  euor2  2138  2moex  2166  2euex  2167  2moswapdc  2170  2exeu  2172  rspe  2582  rsp2e  2584  ceqex  2934  vn0m  3508  intab  3962  copsexg  4342  eusv2nf  4559  dmcosseq  5010  dminss  5158  imainss  5159  relssdmrn  5264  oprabid  6060  tfrlemibxssdm  6536  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  snexxph  7192  nqprl  7814  nqpru  7815  ltsopr  7859  ltexprlemm  7863  recexprlemopl  7888  recexprlemopu  7890  suplocexprlemrl  7980  divsfval  13474