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  2931  vn0m  3504  intab  3955  copsexg  4334  eusv2nf  4551  dmcosseq  5002  dminss  5149  imainss  5150  relssdmrn  5255  oprabid  6045  tfrlemibxssdm  6488  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  snexxph  7140  nqprl  7761  nqpru  7762  ltsopr  7806  ltexprlemm  7810  recexprlemopl  7835  recexprlemopu  7837  suplocexprlemrl  7927  divsfval  13401