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 ⊢ (𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1400  ∃wex 1545

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 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563

This theorem depends on definitions:  df-bi 117

This theorem is referenced 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  3994  copsexg  4379  eusv2nf  4597  dmcosseq  5049  dminss  5197  imainss  5198  relssdmrn  5303  oprabid  6107  tfrlemibxssdm  6588  tfr1onlembxssdm  6604  tfrcllembxssdm  6617  snexxph  7257  nqprl  7908  nqpru  7909  ltsopr  7953  ltexprlemm  7957  recexprlemopl  7982  recexprlemopu  7984  suplocexprlemrl  8074  divsfval  13626