Theorem 19.8a 1639

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 1544	. . . 4 |- ( E. x ph -> A. x E. x ph )
3	2	19.23h 1547	. . 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 1585	1 |- ( ph -> E. x ph )

Syntax hints:   -> wi 4   A.wal 1396   E.wex 1541

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 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.8ad  1640  19.23bi  1641  exim  1648  19.43  1677  hbex  1685  19.2  1687  19.9t  1691  19.9h  1692  excomim  1711  19.38  1724  nexr  1740  sbequ1  1817  equs5e  1844  exdistrfor  1849  sbcof2  1859  mo2n  2108  euor2  2139  2moex  2167  2euex  2168  2moswapdc  2171  2exeu  2173  rspe  2591  rsp2e  2593  ceqex  2944  vn0m  3520  intab  3978  copsexg  4360  eusv2nf  4577  dmcosseq  5029  dminss  5177  imainss  5178  relssdmrn  5283  oprabid  6082  tfrlemibxssdm  6558  tfr1onlembxssdm  6574  tfrcllembxssdm  6587  snexxph  7220  nqprl  7866  nqpru  7867  ltsopr  7911  ltexprlemm  7915  recexprlemopl  7940  recexprlemopu  7942  suplocexprlemrl  8032  divsfval  13541