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 1472	. . . 4 |- ( E. x ph -> A. x E. x ph )
3	2	19.23h 1475	. . 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 1517	1 |- ( ph -> E. x ph )

Syntax hints:   -> wi 4   A.wal 1330   E.wex 1469

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 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488

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  1642  19.38  1655  nexr  1671  sbequ1  1742  equs5e  1768  exdistrfor  1773  sbcof2  1783  mo2n  2028  euor2  2058  2moex  2086  2euex  2087  2moswapdc  2090  2exeu  2092  rspe  2484  rsp2e  2486  ceqex  2816  vn0m  3379  intab  3808  copsexg  4174  eusv2nf  4385  dmcosseq  4818  dminss  4961  imainss  4962  relssdmrn  5067  oprabid  5811  tfrlemibxssdm  6232  tfr1onlembxssdm  6248  tfrcllembxssdm  6261  snexxph  6846  nqprl  7383  nqpru  7384  ltsopr  7428  ltexprlemm  7432  recexprlemopl  7457  recexprlemopu  7459  suplocexprlemrl  7549