Theorem 19.8a 1569

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 1471	. . . 4 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
3	2	19.23h 1474	. . 3 ⊢ (∀𝑥(𝜑 → ∃𝑥𝜑) ↔ (∃𝑥𝜑 → ∃𝑥𝜑))
4	1, 3	mpbir 145	. 2 ⊢ ∀𝑥(𝜑 → ∃𝑥𝜑)
5	4	spi 1516	1 ⊢ (𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1329  ∃wex 1468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.8ad  1570  19.23bi  1571  exim  1578  19.43  1607  hbex  1615  19.2  1617  19.9t  1621  19.9h  1622  excomim  1641  19.38  1654  nexr  1670  sbequ1  1741  equs5e  1767  exdistrfor  1772  sbcof2  1782  mo2n  2025  euor2  2055  2moex  2083  2euex  2084  2moswapdc  2087  2exeu  2089  rspe  2479  rsp2e  2481  ceqex  2807  vn0m  3369  intab  3795  copsexg  4161  eusv2nf  4372  dmcosseq  4805  dminss  4948  imainss  4949  relssdmrn  5054  oprabid  5796  tfrlemibxssdm  6217  tfr1onlembxssdm  6233  tfrcllembxssdm  6246  snexxph  6831  nqprl  7352  nqpru  7353  ltsopr  7397  ltexprlemm  7401  recexprlemopl  7426  recexprlemopu  7428  suplocexprlemrl  7518