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

Theorem 19.8a 1464
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 1365 . . . 4 (xφxxφ)
3219.23h 1368 . . 3 (x(φxφ) ↔ (xφxφ))
41, 3mpbir 134 . 2 x(φxφ)
54spi 1411 1 (φxφ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1226  wex 1362
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 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  19.23bi  1465  exim  1472  19.43  1501  hbex  1509  19.2  1511  19.9t  1515  19.9h  1516  excomim  1535  19.38  1548  nexr  1564  sbequ1  1633  equs5e  1658  exdistrfor  1663  sbcof2  1673  mo2n  1910  euor2  1940  2moex  1968  2euex  1969  2moswapdc  1972  2exeu  1974  rspe  2348  rsp2e  2350  ceqex  2648  vn0m  3209  intab  3618  copsexg  3955  eusv2nf  4138  dmcosseq  4530  dminss  4665  imainss  4666  relssdmrn  4768  oprabid  5461  tfrlemibxssdm  5862  ltsopr  6433  ltexprlemm  6437  recexprlemopl  6459  recexprlemopu  6461
  Copyright terms: Public domain W3C validator