Theorem 19.8a 1522

Description: If a wff is true, 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 1424	. . . 4 |- ( E. x ph -> A. x E. x ph )
3	2	19.23h 1427	. . 3 |- ( A. x ( ph -> E. x ph ) <-> ( E. x ph -> E. x ph ) )
4	1, 3	mpbir 144	. 2 |- A. x ( ph -> E. x ph )
5	4	spi 1469	1 |- ( ph -> E. x ph )

Syntax hints:   -> wi 4   A.wal 1282   E.wex 1421

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  19.23bi  1523  exim  1530  19.43  1559  hbex  1567  19.2  1569  19.9t  1573  19.9h  1574  excomim  1593  19.38  1606  nexr  1622  sbequ1  1691  equs5e  1716  exdistrfor  1721  sbcof2  1731  mo2n  1969  euor2  1999  2moex  2027  2euex  2028  2moswapdc  2031  2exeu  2033  rspe  2412  rsp2e  2414  ceqex  2722  vn0m  3259  intab  3665  copsexg  3999  eusv2nf  4206  dmcosseq  4621  dminss  4758  imainss  4759  relssdmrn  4861  oprabid  5557  tfrlemibxssdm  5964  nqprl  6741  nqpru  6742  ltsopr  6786  ltexprlemm  6790  recexprlemopl  6815  recexprlemopu  6817