Theorem olc 700

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 699	. . 3 |- ( ( ( ps \/ ph ) -> ( ps \/ ph ) ) <-> ( ( ps -> ( ps \/ ph ) ) /\ ( ph -> ( ps \/ ph ) ) ) )
3	1, 2	mpbi 144	. 2 |- ( ( ps -> ( ps \/ ph ) ) /\ ( ph -> ( ps \/ ph ) ) )
4	3	simpri 112	1 |- ( ph -> ( ps \/ ph ) )

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-ia2 106  ax-io 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  oibabs  703  pm1.4  716  olci  721  pm2.07  726  pm2.46  728  biorf  733  pm1.5  754  pm2.41  765  pm4.78i  771  pm3.48  774  ordi  805  andi  807  pm4.72  812  stdcn  832  pm2.54dc  876  pm2.85dc  890  dcor  919  dedlemb  954  xoranor  1355  19.33  1460  hbor  1525  nford  1546  19.30dc  1606  19.43  1607  19.32r  1658  euor2  2055  mooran2  2070  r19.32r  2576  undif3ss  3332  undif4  3420  issod  4236  onsucelsucexmid  4440  sucprcreg  4459  0elnn  4527  acexmidlemph  5760  nntri3or  6382  swoord1  6451  swoord2  6452  exmidaclem  7057  addlocprlem  7336  nqprloc  7346  apreap  8342  zletric  9091  zlelttric  9092  zmulcl  9100  zdceq  9119  zdcle  9120  zdclt  9121  nn0lt2  9125  elnn1uz2  9394  mnflt  9562  mnfltpnf  9564  xrltso  9575  fzdcel  9813  fzm1  9873  qletric  10014  qlelttric  10015  qdceq  10017  nn0o1gt2  11591  bj-fadc  12949  decidin  12993  triap  13213