Theorem olc 665

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 664	. . 3 |- ( ( ( ps \/ ph ) -> ( ps \/ ph ) ) <-> ( ( ps -> ( ps \/ ph ) ) /\ ( ph -> ( ps \/ ph ) ) ) )
3	1, 2	mpbi 143	. 2 |- ( ( ps -> ( ps \/ ph ) ) /\ ( ph -> ( ps \/ ph ) ) )
4	3	simpri 111	1 |- ( ph -> ( ps \/ ph ) )

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-ia2 105  ax-io 663

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm1.4  679  olci  684  pm2.07  689  pm2.46  691  biorf  696  pm1.5  715  pm2.41  726  pm3.48  732  ordi  763  andi  765  pm4.72  770  pm2.54dc  824  oibabs  834  pm4.78i  842  pm2.85dc  845  dcor  877  dedlemb  912  xoranor  1309  19.33  1414  hbor  1479  nford  1500  19.30dc  1559  19.43  1560  19.32r  1611  euor2  2000  mooran2  2015  r19.32r  2502  undif3ss  3232  undif4  3313  issod  4082  onsucelsucexmid  4281  sucprcreg  4300  0elnn  4366  acexmidlemph  5536  nntri3or  6137  swoord1  6201  swoord2  6202  addlocprlem  6787  nqprloc  6797  apreap  7754  zletric  8476  zlelttric  8477  zmulcl  8485  zdceq  8504  zdcle  8505  zdclt  8506  nn0lt2  8510  elnn1uz2  8775  mnflt  8934  mnfltpnf  8936  xrltso  8947  fzdcel  9135  fzm1  9193  qletric  9330  qlelttric  9331  qdceq  9333  nn0o1gt2  10449  decidin  10758