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

Theorem orc 701
Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.)
Assertion
Ref Expression
orc  |-  ( ph  ->  ( ph  \/  ps ) )

Proof of Theorem orc
StepHypRef Expression
1 id 19 . . 3  |-  ( (
ph  \/  ps )  ->  ( ph  \/  ps ) )
2 jaob 699 . . 3  |-  ( ( ( ph  \/  ps )  ->  ( ph  \/  ps ) )  <->  ( ( ph  ->  ( ph  \/  ps ) )  /\  ( ps  ->  ( ph  \/  ps ) ) ) )
31, 2mpbi 144 . 2  |-  ( (
ph  ->  ( ph  \/  ps ) )  /\  ( ps  ->  ( ph  \/  ps ) ) )
43simpli 110 1  |-  ( ph  ->  ( ph  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    \/ wo 697
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-io 698
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm2.67-2  702  pm1.4  716  orci  720  orcd  722  orcs  724  pm2.45  727  biorfi  735  pm1.5  754  pm2.4  767  pm4.44  768  pm4.78i  771  pm4.45  773  pm3.48  774  pm2.76  797  orabs  803  ordi  805  andi  807  pm4.72  812  biort  814  dcim  826  pm2.54dc  876  pm2.85dc  890  dcor  919  pm5.71dc  945  dedlema  953  3mix1  1150  xoranor  1355  19.33  1460  hbor  1525  nford  1546  19.30dc  1606  19.43  1607  19.32r  1658  moor  2070  r19.32r  2578  ssun1  3239  undif3ss  3337  reuun1  3358  prmg  3644  opthpr  3699  exmidn0m  4124  issod  4241  elelsuc  4331  ordtri2or2exmidlem  4441  regexmidlem1  4448  nndceq  6395  nndcel  6396  swoord1  6458  swoord2  6459  addlocprlem  7343  msqge0  8378  mulge0  8381  ltleap  8394  nn1m1nn  8738  elnnz  9064  zletric  9098  zlelttric  9099  zmulcl  9107  zdceq  9126  zdcle  9127  zdclt  9128  ltpnf  9567  xrlttri3  9583  xrpnfdc  9625  xrmnfdc  9626  fzdcel  9820  qletric  10021  qlelttric  10022  qdceq  10024  hashfiv01gt1  10528  isum  11154  nn0o1gt2  11602  bj-trdc  12959  bj-nn0suc0  13148  triap  13224
  Copyright terms: Public domain W3C validator