Theorem 19.8a 1613

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	|- ( ph -> E. x ph )

Proof of Theorem 19.8a

Step	Hyp	Ref	Expression
1		id 19	. . 3 |- ( E. x ph -> E. x ph )
2		hbe1 1518	. . . 4 |- ( E. x ph -> A. x E. x ph )
3	2	19.23h 1521	. . 3 |- ( A. x ( ph -> E. x ph ) <-> ( E. x ph -> E. x ph ) )
4	1, 3	mpbir 146	. 2 |- A. x ( ph -> E. x ph )
5	4	spi 1559	1 |- ( ph -> E. x ph )

Syntax hints:   -> wi 4   A.wal 1371   E.wex 1515

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 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.8ad  1614  19.23bi  1615  exim  1622  19.43  1651  hbex  1659  19.2  1661  19.9t  1665  19.9h  1666  excomim  1686  19.38  1699  nexr  1715  sbequ1  1791  equs5e  1818  exdistrfor  1823  sbcof2  1833  mo2n  2082  euor2  2112  2moex  2140  2euex  2141  2moswapdc  2144  2exeu  2146  rspe  2555  rsp2e  2557  ceqex  2900  vn0m  3472  intab  3914  copsexg  4289  eusv2nf  4504  dmcosseq  4951  dminss  5098  imainss  5099  relssdmrn  5204  oprabid  5978  tfrlemibxssdm  6415  tfr1onlembxssdm  6431  tfrcllembxssdm  6444  snexxph  7054  nqprl  7666  nqpru  7667  ltsopr  7711  ltexprlemm  7715  recexprlemopl  7740  recexprlemopu  7742  suplocexprlemrl  7832  divsfval  13193