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

Step	Hyp	Ref	Expression
1		id 19	. . 3 |- ( ( ps \/ ph ) -> ( ps \/ ph ) )
2		jaob 710	. . 3 |- ( ( ( ps \/ ph ) -> ( ps \/ ph ) ) <-> ( ( ps -> ( ps \/ ph ) ) /\ ( ph -> ( ps \/ ph ) ) ) )
3	1, 2	mpbi 145	. 2 |- ( ( ps -> ( ps \/ ph ) ) /\ ( ph -> ( ps \/ ph ) ) )
4	3	simpri 113	1 |- ( ph -> ( ps \/ ph ) )

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  8543  zletric  9296  zlelttric  9297  zmulcl  9305  zdceq  9327  zdcle  9328  zdclt  9329  nn0lt2  9333  elnn1uz2  9606  mnflt  9782  mnfltpnf  9784  xrltso  9795  fzdcel  10039  fzm1  10099  qletric  10243  qlelttric  10244  qdceq  10246  qsqeqor  10630  nn0o1gt2  11909  prm23lt5  12262  bj-fadc  14476  decidin  14519  triap  14747  tridceq  14774