ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  19.8a Unicode 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.
Assertion
Ref Expression
19.8a

Proof of Theorem 19.8a
StepHypRef Expression
1 id 18 . . 3
2 hbe1 1377 . . . 4
3219.23 1379 . . 3
41, 3mpbir 133 . 2
54a4i 1432 1
Colors of variables: wff set class
Syntax hints:   wi 4  wal 1335  wex 1374
This theorem is referenced by:  19.23bi  1480  exim  1483  19.43  1517  hbex  1528  19.2  1529  19.9  1531  excomim  1533  19.38  1540  nexr  1551  qexmid  1555  exdistrf  1590  sbequ1  1612  equs5e  1632  ax11indn  1813  mo  1845  mo2  1852  euor2  1892  2moex  1895  2euex  1896  2moswap  1899  2exeu  1901  2mo  1902
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-ia1 98  ax-ia2 99  ax-ia3 100  ax-gen 1339  ax-ie1 1375  ax-ie2 1376  ax-4 1392
This theorem depends on definitions:  df-bi 109
  Copyright terms: Public domain W3C validator