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

Theorem 19.8a 1479
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 (φxφ)

Proof of Theorem 19.8a
StepHypRef Expression
1 id 19 . . 3 (xφxφ)
2 hbe1 1381 . . . 4 (xφxxφ)
3219.23h 1384 . . 3 (x(φxφ) ↔ (xφxφ))
41, 3mpbir 134 . 2 x(φxφ)
54spi 1426 1 (φxφ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1240  wex 1378
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  19.23bi  1480  exim  1487  19.43  1516  hbex  1524  19.2  1526  19.9t  1530  19.9h  1531  excomim  1550  19.38  1563  nexr  1579  sbequ1  1648  equs5e  1673  exdistrfor  1678  sbcof2  1688  mo2n  1925  euor2  1955  2moex  1983  2euex  1984  2moswapdc  1987  2exeu  1989  rspe  2364  rsp2e  2366  ceqex  2665  vn0m  3226  intab  3635  copsexg  3972  eusv2nf  4154  dmcosseq  4546  dminss  4681  imainss  4682  relssdmrn  4784  oprabid  5480  tfrlemibxssdm  5882  ltsopr  6568  ltexprlemm  6572  recexprlemopl  6595  recexprlemopu  6597
  Copyright terms: Public domain W3C validator