Theorem 19.8a 1614

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 1519	. . . 4 |- ( E. x ph -> A. x E. x ph )
3	2	19.23h 1522	. . 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 1560	1 |- ( ph -> E. x ph )

Syntax hints:   -> wi 4   A.wal 1371   E.wex 1516

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 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.8ad  1615  19.23bi  1616  exim  1623  19.43  1652  hbex  1660  19.2  1662  19.9t  1666  19.9h  1667  excomim  1687  19.38  1700  nexr  1716  sbequ1  1792  equs5e  1819  exdistrfor  1824  sbcof2  1834  mo2n  2083  euor2  2114  2moex  2142  2euex  2143  2moswapdc  2146  2exeu  2148  rspe  2557  rsp2e  2559  ceqex  2907  vn0m  3480  intab  3928  copsexg  4306  eusv2nf  4521  dmcosseq  4969  dminss  5116  imainss  5117  relssdmrn  5222  oprabid  5999  tfrlemibxssdm  6436  tfr1onlembxssdm  6452  tfrcllembxssdm  6465  snexxph  7078  nqprl  7699  nqpru  7700  ltsopr  7744  ltexprlemm  7748  recexprlemopl  7773  recexprlemopu  7775  suplocexprlemrl  7865  divsfval  13275