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  3397  undif4  3486  issod  4320  onsucelsucexmid  4530  sucprcreg  4549  0elnn  4619  acexmidlemph  5868  nntri3or  6494  swoord1  6564  swoord2  6565  exmidaclem  7207  exmidontri2or  7242  addlocprlem  7534  nqprloc  7544  apreap  8544  zletric  9297  zlelttric  9298  zmulcl  9306  zdceq  9328  zdcle  9329  zdclt  9330  nn0lt2  9334  elnn1uz2  9607  mnflt  9783  mnfltpnf  9785  xrltso  9796  fzdcel  10040  fzm1  10100  qletric  10244  qlelttric  10245  qdceq  10247  qsqeqor  10631  nn0o1gt2  11910  prm23lt5  12263  bj-fadc  14509  decidin  14552  triap  14780  tridceq  14807