Theorem 19.8a 1604

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 1509	. . . 4 |- ( E. x ph -> A. x E. x ph )
3	2	19.23h 1512	. . 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 1550	1 |- ( ph -> E. x ph )

Syntax hints:   -> wi 4   A.wal 1362   E.wex 1506

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 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.8ad  1605  19.23bi  1606  exim  1613  19.43  1642  hbex  1650  19.2  1652  19.9t  1656  19.9h  1657  excomim  1677  19.38  1690  nexr  1706  sbequ1  1782  equs5e  1809  exdistrfor  1814  sbcof2  1824  mo2n  2073  euor2  2103  2moex  2131  2euex  2132  2moswapdc  2135  2exeu  2137  rspe  2546  rsp2e  2548  ceqex  2891  vn0m  3462  intab  3903  copsexg  4277  eusv2nf  4491  dmcosseq  4937  dminss  5084  imainss  5085  relssdmrn  5190  oprabid  5954  tfrlemibxssdm  6385  tfr1onlembxssdm  6401  tfrcllembxssdm  6414  snexxph  7016  nqprl  7618  nqpru  7619  ltsopr  7663  ltexprlemm  7667  recexprlemopl  7692  recexprlemopu  7694  suplocexprlemrl  7784  divsfval  12971