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

Theorem 19.8a 1523
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 1425 . . . 4  |-  ( E. x ph  ->  A. x E. x ph )
3219.23h 1428 . . 3  |-  ( A. x ( ph  ->  E. x ph )  <->  ( E. x ph  ->  E. x ph ) )
41, 3mpbir 144 . 2  |-  A. x
( ph  ->  E. x ph )
54spi 1470 1  |-  ( ph  ->  E. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1283   E.wex 1422
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 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  19.23bi  1524  exim  1531  19.43  1560  hbex  1568  19.2  1570  19.9t  1574  19.9h  1575  excomim  1594  19.38  1607  nexr  1623  sbequ1  1692  equs5e  1717  exdistrfor  1722  sbcof2  1732  mo2n  1970  euor2  2000  2moex  2028  2euex  2029  2moswapdc  2032  2exeu  2034  rspe  2413  rsp2e  2415  ceqex  2723  vn0m  3266  intab  3673  copsexg  4007  eusv2nf  4214  dmcosseq  4631  dminss  4768  imainss  4769  relssdmrn  4871  oprabid  5568  tfrlemibxssdm  5976  tfr1onlembxssdm  5992  tfrcllembxssdm  6005  nqprl  6803  nqpru  6804  ltsopr  6848  ltexprlemm  6852  recexprlemopl  6877  recexprlemopu  6879
  Copyright terms: Public domain W3C validator