Theorem olc 716

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 715	. . 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 713

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  oibabs  719  pm1.4  732  olci  737  pm2.07  742  pm2.46  744  biorf  749  pm1.5  770  pm2.41  781  pm4.78i  787  pm3.48  790  ordi  821  andi  823  pm4.72  832  stdcn  852  pm2.54dc  896  pm2.85dc  910  dcor  941  dedlemb  976  anifpdc  992  xoranor  1419  19.33  1530  hbor  1592  nford  1613  19.30dc  1673  19.43  1674  19.32r  1726  euor2  2136  mooran2  2151  r19.32r  2677  undif3ss  3465  undif4  3554  issod  4410  onsucelsucexmid  4622  sucprcreg  4641  0elnn  4711  acexmidlemph  5994  nntri3or  6639  swoord1  6709  swoord2  6710  exmidaclem  7390  exmidontri2or  7428  addlocprlem  7722  nqprloc  7732  apreap  8734  zletric  9490  zlelttric  9491  zmulcl  9500  zdceq  9522  zdcle  9523  zdclt  9524  nn0lt2  9528  elnn1uz2  9802  mnflt  9979  mnfltpnf  9981  xrltso  9992  fzdcel  10236  fzm1  10296  qletric  10461  qlelttric  10462  qdceq  10464  qdclt  10465  qsqeqor  10872  zzlesq  10930  nn0o1gt2  12416  prm23lt5  12786  gausslemma2dlem0f  15733  umgrupgr  15912  umgrislfupgrenlem  15928  usgruspgr  15981  bj-fadc  16118  decidin  16161  triap  16397  tridceq  16424