Theorem 19.8a 1643

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1400  ∃wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563

This proof depends on definitions:  df-bi 117

This theorem is used by:  19.8ad  1644  19.23bi  1645  exim  1652  19.43  1681  hbex  1689  19.2  1691  19.9t  1695  19.9h  1696  excomim  1715  19.38  1728  nexr  1744  sbequ1  1821  equs5e  1848  exdistrfor  1853  sbcof2  1863  mo2n  2114  euor2  2145  2moex  2173  2euex  2174  2moswapdc  2177  2exeu  2179  rspe  2599  rsp2e  2601  ceqex  2953  vn0m  3533  intab  3999  copsexg  4386  eusv2nf  4604  dmcosseq  5056  dminss  5205  imainss  5206  relssdmrn  5311  oprabid  6120  tfrlemibxssdm  6602  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  snexxph  7272  nqprl  7924  nqpru  7925  ltsopr  7969  ltexprlemm  7973  recexprlemopl  7998  recexprlemopu  8000  suplocexprlemrl  8090  divsfval  13708