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  3463  intab  3904  copsexg  4278  eusv2nf  4492  dmcosseq  4938  dminss  5085  imainss  5086  relssdmrn  5191  oprabid  5957  tfrlemibxssdm  6394  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  snexxph  7025  nqprl  7635  nqpru  7636  ltsopr  7680  ltexprlemm  7684  recexprlemopl  7709  recexprlemopu  7711  suplocexprlemrl  7801  divsfval  13030