Theorem olc 712

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 711	. . 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 709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-io 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  oibabs  715  pm1.4  728  olci  733  pm2.07  738  pm2.46  740  biorf  745  pm1.5  766  pm2.41  777  pm4.78i  783  pm3.48  786  ordi  817  andi  819  pm4.72  828  stdcn  848  pm2.54dc  892  pm2.85dc  906  dcor  937  dedlemb  972  xoranor  1388  19.33  1498  hbor  1560  nford  1581  19.30dc  1641  19.43  1642  19.32r  1694  euor2  2103  mooran2  2118  r19.32r  2643  undif3ss  3425  undif4  3514  issod  4355  onsucelsucexmid  4567  sucprcreg  4586  0elnn  4656  acexmidlemph  5918  nntri3or  6560  swoord1  6630  swoord2  6631  exmidaclem  7293  exmidontri2or  7328  addlocprlem  7621  nqprloc  7631  apreap  8633  zletric  9389  zlelttric  9390  zmulcl  9398  zdceq  9420  zdcle  9421  zdclt  9422  nn0lt2  9426  elnn1uz2  9700  mnflt  9877  mnfltpnf  9879  xrltso  9890  fzdcel  10134  fzm1  10194  qletric  10350  qlelttric  10351  qdceq  10353  qdclt  10354  qsqeqor  10761  zzlesq  10819  nn0o1gt2  12089  prm23lt5  12459  gausslemma2dlem0f  15403  bj-fadc  15508  decidin  15551  triap  15786  tridceq  15813