Theorem 19.8a 1525

Description: If a wff is true, 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 1427	. . . 4 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
3	2	19.23h 1430	. . 3 ⊢ (∀𝑥(𝜑 → ∃𝑥𝜑) ↔ (∃𝑥𝜑 → ∃𝑥𝜑))
4	1, 3	mpbir 144	. 2 ⊢ ∀𝑥(𝜑 → ∃𝑥𝜑)
5	4	spi 1472	1 ⊢ (𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1285  ∃wex 1424

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  19.23bi  1526  exim  1533  19.43  1562  hbex  1570  19.2  1572  19.9t  1576  19.9h  1577  excomim  1596  19.38  1609  nexr  1625  sbequ1  1695  equs5e  1720  exdistrfor  1725  sbcof2  1735  mo2n  1973  euor2  2003  2moex  2031  2euex  2032  2moswapdc  2035  2exeu  2037  rspe  2420  rsp2e  2422  ceqex  2735  vn0m  3283  intab  3700  copsexg  4045  eusv2nf  4252  dmcosseq  4672  dminss  4812  imainss  4813  relssdmrn  4917  oprabid  5638  tfrlemibxssdm  6046  tfr1onlembxssdm  6062  tfrcllembxssdm  6075  snexxph  6608  nqprl  7054  nqpru  7055  ltsopr  7099  ltexprlemm  7103  recexprlemopl  7128  recexprlemopu  7130