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

Theorem 19.8a 1590
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 1495 . . . 4  |-  ( E. x ph  ->  A. x E. x ph )
3219.23h 1498 . . 3  |-  ( A. x ( ph  ->  E. x ph )  <->  ( E. x ph  ->  E. x ph ) )
41, 3mpbir 146 . 2  |-  A. x
( ph  ->  E. x ph )
54spi 1536 1  |-  ( ph  ->  E. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1351   E.wex 1492
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 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  19.8ad  1591  19.23bi  1592  exim  1599  19.43  1628  hbex  1636  19.2  1638  19.9t  1642  19.9h  1643  excomim  1663  19.38  1676  nexr  1692  sbequ1  1768  equs5e  1795  exdistrfor  1800  sbcof2  1810  mo2n  2054  euor2  2084  2moex  2112  2euex  2113  2moswapdc  2116  2exeu  2118  rspe  2526  rsp2e  2528  ceqex  2864  vn0m  3434  intab  3871  copsexg  4241  eusv2nf  4453  dmcosseq  4894  dminss  5039  imainss  5040  relssdmrn  5145  oprabid  5901  tfrlemibxssdm  6322  tfr1onlembxssdm  6338  tfrcllembxssdm  6351  snexxph  6943  nqprl  7541  nqpru  7542  ltsopr  7586  ltexprlemm  7590  recexprlemopl  7615  recexprlemopu  7617  suplocexprlemrl  7707
  Copyright terms: Public domain W3C validator