Theorem 19.8a 1569

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 1471	. . . 4 |- ( E. x ph -> A. x E. x ph )
3	2	19.23h 1474	. . 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 1329   E.wex 1468

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 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.8ad  1570  19.23bi  1571  exim  1578  19.43  1607  hbex  1615  19.2  1617  19.9t  1621  19.9h  1622  excomim  1641  19.38  1654  nexr  1670  sbequ1  1741  equs5e  1767  exdistrfor  1772  sbcof2  1782  mo2n  2027  euor2  2057  2moex  2085  2euex  2086  2moswapdc  2089  2exeu  2091  rspe  2481  rsp2e  2483  ceqex  2812  vn0m  3374  intab  3800  copsexg  4166  eusv2nf  4377  dmcosseq  4810  dminss  4953  imainss  4954  relssdmrn  5059  oprabid  5803  tfrlemibxssdm  6224  tfr1onlembxssdm  6240  tfrcllembxssdm  6253  snexxph  6838  nqprl  7359  nqpru  7360  ltsopr  7404  ltexprlemm  7408  recexprlemopl  7433  recexprlemopu  7435  suplocexprlemrl  7525