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  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