Theorem 19.8a 1578

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

Syntax hints:   → wi 4  ∀wal 1341  ∃wex 1480

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 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.8ad  1579  19.23bi  1580  exim  1587  19.43  1616  hbex  1624  19.2  1626  19.9t  1630  19.9h  1631  excomim  1651  19.38  1664  nexr  1680  sbequ1  1756  equs5e  1783  exdistrfor  1788  sbcof2  1798  mo2n  2042  euor2  2072  2moex  2100  2euex  2101  2moswapdc  2104  2exeu  2106  rspe  2515  rsp2e  2517  ceqex  2853  vn0m  3420  intab  3853  copsexg  4222  eusv2nf  4434  dmcosseq  4875  dminss  5018  imainss  5019  relssdmrn  5124  oprabid  5874  tfrlemibxssdm  6295  tfr1onlembxssdm  6311  tfrcllembxssdm  6324  snexxph  6915  nqprl  7492  nqpru  7493  ltsopr  7537  ltexprlemm  7541  recexprlemopl  7566  recexprlemopu  7568  suplocexprlemrl  7658