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

Theorem olc 631
Description: Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.)
Assertion
Ref Expression
olc

Proof of Theorem olc
StepHypRef Expression
1 id 19 . . 3
2 jaob 630 . . 3
31, 2mpbi 133 . 2
43simpri 106 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wo 628
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-io 629
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm1.4  645  olci  650  pm2.07  655  pm2.46  657  biorf  662  pm1.5  681  pm2.41  692  pm3.48  698  ordi  728  andi  730  pm4.72  735  pm2.54dc  789  oibabs  799  pm4.78i  807  pm2.85dc  810  dcor  842  dedlemb  876  xoranor  1267  19.33  1370  hbor  1435  nford  1456  19.30dc  1515  19.43  1516  19.32r  1567  euor2  1955  mooran2  1970  r19.32r  2451  undif3ss  3192  undif4  3278  issod  4047  onsucelsucexmid  4215  sucprcreg  4227  0elnn  4283  acexmidlemph  5448  nntri3or  6011  swoord1  6071  swoord2  6072  addlocprlem  6518  nqprloc  6528  apreap  7371  zletric  8065  zlelttric  8066  zmulcl  8073  zdceq  8092  zdcle  8093  zdclt  8094  nn0lt2  8098  elnn1uz2  8320  mnflt  8474  mnfltpnf  8476  xrltso  8487  fzdcel  8674  fzm1  8732
  Copyright terms: Public domain W3C validator