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  4288  eusv2nf  4503  dmcosseq  4950  dminss  5097  imainss  5098  relssdmrn  5203  oprabid  5976  tfrlemibxssdm  6413  tfr1onlembxssdm  6429  tfrcllembxssdm  6442  snexxph  7052  nqprl  7664  nqpru  7665  ltsopr  7709  ltexprlemm  7713  recexprlemopl  7738  recexprlemopu  7740  suplocexprlemrl  7830  divsfval  13160