Theorem 19.8a 1577

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 1482	. . . 4 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
3	2	19.23h 1485	. . 3 ⊢ (∀𝑥(𝜑 → ∃𝑥𝜑) ↔ (∃𝑥𝜑 → ∃𝑥𝜑))
4	1, 3	mpbir 145	. 2 ⊢ ∀𝑥(𝜑 → ∃𝑥𝜑)
5	4	spi 1523	1 ⊢ (𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1340  ∃wex 1479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.8ad  1578  19.23bi  1579  exim  1586  19.43  1615  hbex  1623  19.2  1625  19.9t  1629  19.9h  1630  excomim  1650  19.38  1663  nexr  1679  sbequ1  1755  equs5e  1782  exdistrfor  1787  sbcof2  1797  mo2n  2041  euor2  2071  2moex  2099  2euex  2100  2moswapdc  2103  2exeu  2105  rspe  2513  rsp2e  2515  ceqex  2848  vn0m  3415  intab  3847  copsexg  4216  eusv2nf  4428  dmcosseq  4869  dminss  5012  imainss  5013  relssdmrn  5118  oprabid  5865  tfrlemibxssdm  6286  tfr1onlembxssdm  6302  tfrcllembxssdm  6315  snexxph  6906  nqprl  7483  nqpru  7484  ltsopr  7528  ltexprlemm  7532  recexprlemopl  7557  recexprlemopu  7559  suplocexprlemrl  7649