Theorem 19.8a 1570

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 1475	. . . 4 |- ( E. x ph -> A. x E. x ph )
3	2	19.23h 1478	. . 3 |- ( A. x ( ph -> E. x ph ) <-> ( E. x ph -> E. x ph ) )
4	1, 3	mpbir 145	. 2 |- A. x ( ph -> E. x ph )
5	4	spi 1516	1 |- ( ph -> E. x ph )

Syntax hints:   -> wi 4   A.wal 1333   E.wex 1472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.8ad  1571  19.23bi  1572  exim  1579  19.43  1608  hbex  1616  19.2  1618  19.9t  1622  19.9h  1623  excomim  1643  19.38  1656  nexr  1672  sbequ1  1748  equs5e  1775  exdistrfor  1780  sbcof2  1790  mo2n  2034  euor2  2064  2moex  2092  2euex  2093  2moswapdc  2096  2exeu  2098  rspe  2506  rsp2e  2508  ceqex  2839  vn0m  3405  intab  3836  copsexg  4204  eusv2nf  4415  dmcosseq  4856  dminss  4999  imainss  5000  relssdmrn  5105  oprabid  5850  tfrlemibxssdm  6271  tfr1onlembxssdm  6287  tfrcllembxssdm  6300  snexxph  6891  nqprl  7465  nqpru  7466  ltsopr  7510  ltexprlemm  7514  recexprlemopl  7539  recexprlemopu  7541  suplocexprlemrl  7631