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  3951  copsexg  4329  eusv2nf  4546  dmcosseq  4995  dminss  5142  imainss  5143  relssdmrn  5248  oprabid  6032  tfrlemibxssdm  6471  tfr1onlembxssdm  6487  tfrcllembxssdm  6500  snexxph  7113  nqprl  7734  nqpru  7735  ltsopr  7779  ltexprlemm  7783  recexprlemopl  7808  recexprlemopu  7810  suplocexprlemrl  7900  divsfval  13356