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  1817  equs5e  1844  exdistrfor  1849  sbcof2  1859  mo2n  2110  euor2  2141  2moex  2169  2euex  2170  2moswapdc  2173  2exeu  2175  rspe  2593  rsp2e  2595  ceqex  2947  vn0m  3524  intab  3983  copsexg  4365  eusv2nf  4582  dmcosseq  5034  dminss  5182  imainss  5183  relssdmrn  5288  oprabid  6090  tfrlemibxssdm  6571  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  snexxph  7233  nqprl  7882  nqpru  7883  ltsopr  7927  ltexprlemm  7931  recexprlemopl  7956  recexprlemopu  7958  suplocexprlemrl  8048  divsfval  13592