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  6000  nntri3or  6647  swoord1  6717  swoord2  6718  exmidaclem  7398  exmidontri2or  7436  addlocprlem  7730  nqprloc  7740  apreap  8742  zletric  9498  zlelttric  9499  zmulcl  9508  zdceq  9530  zdcle  9531  zdclt  9532  nn0lt2  9536  elnn1uz2  9810  mnflt  9987  mnfltpnf  9989  xrltso  10000  fzdcel  10244  fzm1  10304  qletric  10469  qlelttric  10470  qdceq  10472  qdclt  10473  qsqeqor  10880  zzlesq  10938  nn0o1gt2  12424  prm23lt5  12794  gausslemma2dlem0f  15741  umgrupgr  15920  umgrislfupgrenlem  15936  usgruspgr  15989  bj-fadc  16142  decidin  16185  triap  16424  tridceq  16451