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

Theorem orc 666
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 664 . . 3  |-  ( ( ( ph  \/  ps )  ->  ( ph  \/  ps ) )  <->  ( ( ph  ->  ( ph  \/  ps ) )  /\  ( ps  ->  ( ph  \/  ps ) ) ) )
31, 2mpbi 143 . 2  |-  ( (
ph  ->  ( ph  \/  ps ) )  /\  ( ps  ->  ( ph  \/  ps ) ) )
43simpli 109 1  |-  ( ph  ->  ( ph  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    \/ wo 662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm2.67-2  667  pm1.4  679  orci  683  orcd  685  orcs  687  pm2.45  690  biorfi  698  pm1.5  715  pm2.4  728  pm4.44  729  pm4.45  731  pm3.48  732  pm2.76  755  orabs  761  ordi  763  andi  765  pm4.72  770  biort  772  dcim  818  pm2.54dc  824  pm4.78i  842  pm2.85dc  845  dcor  877  pm5.71dc  903  dedlema  911  3mix1  1108  xoranor  1309  19.33  1414  hbor  1479  nford  1500  19.30dc  1559  19.43  1560  19.32r  1611  moor  2013  r19.32r  2502  ssun1  3136  undif3ss  3232  reuun1  3253  prmg  3519  opthpr  3572  issod  4082  elelsuc  4172  ordtri2or2exmidlem  4277  regexmidlem1  4284  nndceq  6143  nndcel  6144  swoord1  6201  swoord2  6202  addlocprlem  6787  msqge0  7783  mulge0  7786  ltleap  7797  nn1m1nn  8124  elnnz  8442  zletric  8476  zlelttric  8477  zmulcl  8485  zdceq  8504  zdcle  8505  zdclt  8506  ltpnf  8932  xrlttri3  8948  fzdcel  9135  qletric  9330  qlelttric  9331  qdceq  9333  sizefiv01gt1  9806  nn0o1gt2  10449  bj-nn0suc0  10903
  Copyright terms: Public domain W3C validator