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  4384  eusv2nf  4602  dmcosseq  5054  dminss  5202  imainss  5203  relssdmrn  5308  oprabid  6117  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  snexxph  7267  nqprl  7918  nqpru  7919  ltsopr  7963  ltexprlemm  7967  recexprlemopl  7992  recexprlemopu  7994  suplocexprlemrl  8084  divsfval  13649