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  7919  nqpru  7920  ltsopr  7964  ltexprlemm  7968  recexprlemopl  7993  recexprlemopu  7995  suplocexprlemrl  8085  divsfval  13702