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

Theorem olc 711
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 710 . . 3  |-  ( ( ( ps  \/  ph )  ->  ( ps  \/  ph ) )  <->  ( ( ps  ->  ( ps  \/  ph ) )  /\  ( ph  ->  ( ps  \/  ph ) ) ) )
31, 2mpbi 145 . 2  |-  ( ( ps  ->  ( ps  \/  ph ) )  /\  ( ph  ->  ( ps  \/  ph ) ) )
43simpri 113 1  |-  ( ph  ->  ( ps  \/  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    \/ wo 708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-io 709
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  oibabs  714  pm1.4  727  olci  732  pm2.07  737  pm2.46  739  biorf  744  pm1.5  765  pm2.41  776  pm4.78i  782  pm3.48  785  ordi  816  andi  818  pm4.72  827  stdcn  847  pm2.54dc  891  pm2.85dc  905  dcor  935  dedlemb  970  xoranor  1377  19.33  1484  hbor  1546  nford  1567  19.30dc  1627  19.43  1628  19.32r  1680  euor2  2084  mooran2  2099  r19.32r  2623  undif3ss  3396  undif4  3485  issod  4319  onsucelsucexmid  4529  sucprcreg  4548  0elnn  4618  acexmidlemph  5867  nntri3or  6493  swoord1  6563  swoord2  6564  exmidaclem  7206  exmidontri2or  7241  addlocprlem  7533  nqprloc  7543  apreap  8542  zletric  9295  zlelttric  9296  zmulcl  9304  zdceq  9326  zdcle  9327  zdclt  9328  nn0lt2  9332  elnn1uz2  9605  mnflt  9781  mnfltpnf  9783  xrltso  9794  fzdcel  10037  fzm1  10097  qletric  10241  qlelttric  10242  qdceq  10244  qsqeqor  10627  nn0o1gt2  11904  prm23lt5  12257  bj-fadc  14388  decidin  14431  triap  14659  tridceq  14686
  Copyright terms: Public domain W3C validator