Theorem 19.8a 1636

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

Syntax hints:   → wi 4  ∀wal 1393  ∃wex 1538

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 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.8ad  1637  19.23bi  1638  exim  1645  19.43  1674  hbex  1682  19.2  1684  19.9t  1688  19.9h  1689  excomim  1709  19.38  1722  nexr  1738  sbequ1  1814  equs5e  1841  exdistrfor  1846  sbcof2  1856  mo2n  2105  euor2  2136  2moex  2164  2euex  2165  2moswapdc  2168  2exeu  2170  rspe  2579  rsp2e  2581  ceqex  2930  vn0m  3503  intab  3952  copsexg  4330  eusv2nf  4547  dmcosseq  4996  dminss  5143  imainss  5144  relssdmrn  5249  oprabid  6039  tfrlemibxssdm  6479  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  snexxph  7128  nqprl  7749  nqpru  7750  ltsopr  7794  ltexprlemm  7798  recexprlemopl  7823  recexprlemopu  7825  suplocexprlemrl  7915  divsfval  13376