ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  19.8a Unicode version

Theorem 19.8a 1552
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
StepHypRef Expression
1 id 19 . . 3  |-  ( E. x ph  ->  E. x ph )
2 hbe1 1454 . . . 4  |-  ( E. x ph  ->  A. x E. x ph )
3219.23h 1457 . . 3  |-  ( A. x ( ph  ->  E. x ph )  <->  ( E. x ph  ->  E. x ph ) )
41, 3mpbir 145 . 2  |-  A. x
( ph  ->  E. x ph )
54spi 1499 1  |-  ( ph  ->  E. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1312   E.wex 1451
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 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  19.8ad  1553  19.23bi  1554  exim  1561  19.43  1590  hbex  1598  19.2  1600  19.9t  1604  19.9h  1605  excomim  1624  19.38  1637  nexr  1653  sbequ1  1724  equs5e  1749  exdistrfor  1754  sbcof2  1764  mo2n  2003  euor2  2033  2moex  2061  2euex  2062  2moswapdc  2065  2exeu  2067  rspe  2456  rsp2e  2458  ceqex  2784  vn0m  3342  intab  3768  copsexg  4134  eusv2nf  4345  dmcosseq  4778  dminss  4921  imainss  4922  relssdmrn  5027  oprabid  5769  tfrlemibxssdm  6190  tfr1onlembxssdm  6206  tfrcllembxssdm  6219  snexxph  6804  nqprl  7323  nqpru  7324  ltsopr  7368  ltexprlemm  7372  recexprlemopl  7397  recexprlemopu  7399  suplocexprlemrl  7489
  Copyright terms: Public domain W3C validator