Theorem 19.8a 1638

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

Syntax hints:   → wi 4  ∀wal 1395  ∃wex 1540

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 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.8ad  1639  19.23bi  1640  exim  1647  19.43  1676  hbex  1684  19.2  1686  19.9t  1690  19.9h  1691  excomim  1711  19.38  1724  nexr  1740  sbequ1  1816  equs5e  1843  exdistrfor  1848  sbcof2  1858  mo2n  2107  euor2  2138  2moex  2166  2euex  2167  2moswapdc  2170  2exeu  2172  rspe  2581  rsp2e  2583  ceqex  2933  vn0m  3506  intab  3957  copsexg  4336  eusv2nf  4553  dmcosseq  5004  dminss  5151  imainss  5152  relssdmrn  5257  oprabid  6050  tfrlemibxssdm  6493  tfr1onlembxssdm  6509  tfrcllembxssdm  6522  snexxph  7149  nqprl  7771  nqpru  7772  ltsopr  7816  ltexprlemm  7820  recexprlemopl  7845  recexprlemopu  7847  suplocexprlemrl  7937  divsfval  13416