Theorem 19.8a 1590

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 1495	. . . 4 |- ( E. x ph -> A. x E. x ph )
3	2	19.23h 1498	. . 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 1536	1 |- ( ph -> E. x ph )

Syntax hints:   -> wi 4   A.wal 1351   E.wex 1492

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 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.8ad  1591  19.23bi  1592  exim  1599  19.43  1628  hbex  1636  19.2  1638  19.9t  1642  19.9h  1643  excomim  1663  19.38  1676  nexr  1692  sbequ1  1768  equs5e  1795  exdistrfor  1800  sbcof2  1810  mo2n  2054  euor2  2084  2moex  2112  2euex  2113  2moswapdc  2116  2exeu  2118  rspe  2526  rsp2e  2528  ceqex  2864  vn0m  3434  intab  3872  copsexg  4242  eusv2nf  4454  dmcosseq  4895  dminss  5040  imainss  5041  relssdmrn  5146  oprabid  5902  tfrlemibxssdm  6323  tfr1onlembxssdm  6339  tfrcllembxssdm  6352  snexxph  6944  nqprl  7545  nqpru  7546  ltsopr  7590  ltexprlemm  7594  recexprlemopl  7619  recexprlemopu  7621  suplocexprlemrl  7711