Theorem 19.8a 1614

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 1519	. . . 4 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
3	2	19.23h 1522	. . 3 ⊢ (∀𝑥(𝜑 → ∃𝑥𝜑) ↔ (∃𝑥𝜑 → ∃𝑥𝜑))
4	1, 3	mpbir 146	. 2 ⊢ ∀𝑥(𝜑 → ∃𝑥𝜑)
5	4	spi 1560	1 ⊢ (𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1371  ∃wex 1516

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 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.8ad  1615  19.23bi  1616  exim  1623  19.43  1652  hbex  1660  19.2  1662  19.9t  1666  19.9h  1667  excomim  1687  19.38  1700  nexr  1716  sbequ1  1792  equs5e  1819  exdistrfor  1824  sbcof2  1834  mo2n  2083  euor2  2113  2moex  2141  2euex  2142  2moswapdc  2145  2exeu  2147  rspe  2556  rsp2e  2558  ceqex  2904  vn0m  3476  intab  3919  copsexg  4295  eusv2nf  4510  dmcosseq  4958  dminss  5105  imainss  5106  relssdmrn  5211  oprabid  5988  tfrlemibxssdm  6425  tfr1onlembxssdm  6441  tfrcllembxssdm  6454  snexxph  7066  nqprl  7679  nqpru  7680  ltsopr  7724  ltexprlemm  7728  recexprlemopl  7753  recexprlemopu  7755  suplocexprlemrl  7845  divsfval  13230