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

Theorem olc 683
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  |-  ( ph  ->  ( ps  \/  ph ) )

Proof of Theorem olc
StepHypRef Expression
1 id 19 . . 3  |-  ( ( ps  \/  ph )  ->  ( ps  \/  ph ) )
2 jaob 682 . . 3  |-  ( ( ( ps  \/  ph )  ->  ( ps  \/  ph ) )  <->  ( ( ps  ->  ( ps  \/  ph ) )  /\  ( ph  ->  ( ps  \/  ph ) ) ) )
31, 2mpbi 144 . 2  |-  ( ( ps  ->  ( ps  \/  ph ) )  /\  ( ph  ->  ( ps  \/  ph ) ) )
43simpri 112 1  |-  ( ph  ->  ( ps  \/  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    \/ wo 680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-io 681
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  oibabs  686  pm1.4  699  olci  704  pm2.07  709  pm2.46  711  biorf  716  pm1.5  737  pm2.41  748  pm4.78i  754  pm3.48  757  ordi  788  andi  790  pm4.72  795  stdcn  815  pm2.54dc  859  pm2.85dc  873  dcor  902  dedlemb  937  xoranor  1338  19.33  1443  hbor  1508  nford  1529  19.30dc  1589  19.43  1590  19.32r  1641  euor2  2033  mooran2  2048  r19.32r  2553  undif3ss  3305  undif4  3393  issod  4209  onsucelsucexmid  4413  sucprcreg  4432  0elnn  4500  acexmidlemph  5733  nntri3or  6355  swoord1  6424  swoord2  6425  exmidaclem  7028  addlocprlem  7307  nqprloc  7317  apreap  8312  zletric  9049  zlelttric  9050  zmulcl  9058  zdceq  9077  zdcle  9078  zdclt  9079  nn0lt2  9083  elnn1uz2  9350  mnflt  9509  mnfltpnf  9511  xrltso  9522  fzdcel  9760  fzm1  9820  qletric  9961  qlelttric  9962  qdceq  9964  nn0o1gt2  11498  bj-fadc  12771  decidin  12815  triap  13035
  Copyright terms: Public domain W3C validator