Theorem olc 719

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 718	. . 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 716

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  oibabs  722  pm1.4  735  olci  740  pm2.07  745  pm2.46  747  biorf  752  pm1.5  773  pm2.41  784  pm4.78i  790  pm3.48  793  ordi  824  andi  826  pm4.72  835  stdcn  855  pm2.54dc  899  pm2.85dc  913  dcor  944  dedlemb  979  anifpdc  995  xoranor  1422  19.33  1533  hbor  1595  nford  1616  19.30dc  1676  19.43  1677  19.32r  1728  euor2  2141  mooran2  2156  r19.32r  2691  undif3ss  3486  undif4  3575  issod  4445  onsucelsucexmid  4657  sucprcreg  4676  0elnn  4746  acexmidlemph  6051  nntri3or  6739  swoord1  6809  swoord2  6810  exmidaclem  7528  exmidontri2or  7566  addlocprlem  7866  nqprloc  7876  apreap  8879  zletric  9641  zlelttric  9642  zmulcl  9651  zdceq  9673  zdcle  9674  zdclt  9675  nn0lt2  9680  elnn1uz2  9960  mnflt  10138  mnfltpnf  10140  xrltso  10151  fzdcel  10397  fzm1  10459  qletric  10628  qlelttric  10629  qdceq  10631  qdclt  10632  qsqeqor  11039  zzlesq  11098  nn0o1gt2  12619  prm23lt5  12989  gausslemma2dlem0f  16056  umgrupgr  16236  umgrislfupgrenlem  16254  usgruspgr  16307  konigsbergssiedgwen  16610  bj-fadc  16665  decidin  16708  triap  16952  tridceq  16980