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

Theorem 19.8a 1527
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
StepHypRef Expression
1 id 19 . . 3  |-  ( E. x ph  ->  E. x ph )
2 hbe1 1429 . . . 4  |-  ( E. x ph  ->  A. x E. x ph )
3219.23h 1432 . . 3  |-  ( A. x ( ph  ->  E. x ph )  <->  ( E. x ph  ->  E. x ph ) )
41, 3mpbir 144 . 2  |-  A. x
( ph  ->  E. x ph )
54spi 1474 1  |-  ( ph  ->  E. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1287   E.wex 1426
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 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  19.23bi  1528  exim  1535  19.43  1564  hbex  1572  19.2  1574  19.9t  1578  19.9h  1579  excomim  1598  19.38  1611  nexr  1627  sbequ1  1698  equs5e  1723  exdistrfor  1728  sbcof2  1738  mo2n  1976  euor2  2006  2moex  2034  2euex  2035  2moswapdc  2038  2exeu  2040  rspe  2424  rsp2e  2426  ceqex  2742  vn0m  3292  intab  3712  copsexg  4062  eusv2nf  4269  dmcosseq  4692  dminss  4833  imainss  4834  relssdmrn  4938  oprabid  5663  tfrlemibxssdm  6074  tfr1onlembxssdm  6090  tfrcllembxssdm  6103  snexxph  6638  nqprl  7089  nqpru  7090  ltsopr  7134  ltexprlemm  7138  recexprlemopl  7163  recexprlemopu  7165
  Copyright terms: Public domain W3C validator