Theorem olc 706

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 705	. . 3 |- ( ( ( ps \/ ph ) -> ( ps \/ ph ) ) <-> ( ( ps -> ( ps \/ ph ) ) /\ ( ph -> ( ps \/ ph ) ) ) )
3	1, 2	mpbi 144	. 2 |- ( ( ps -> ( ps \/ ph ) ) /\ ( ph -> ( ps \/ ph ) ) )
4	3	simpri 112	1 |- ( ph -> ( ps \/ ph ) )

Syntax hints:   -> wi 4   /\ wa 103   \/ wo 703

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  oibabs  709  pm1.4  722  olci  727  pm2.07  732  pm2.46  734  biorf  739  pm1.5  760  pm2.41  771  pm4.78i  777  pm3.48  780  ordi  811  andi  813  pm4.72  822  stdcn  842  pm2.54dc  886  pm2.85dc  900  dcor  930  dedlemb  965  xoranor  1372  19.33  1477  hbor  1539  nford  1560  19.30dc  1620  19.43  1621  19.32r  1673  euor2  2077  mooran2  2092  r19.32r  2616  undif3ss  3388  undif4  3477  issod  4304  onsucelsucexmid  4514  sucprcreg  4533  0elnn  4603  acexmidlemph  5846  nntri3or  6472  swoord1  6542  swoord2  6543  exmidaclem  7185  exmidontri2or  7220  addlocprlem  7497  nqprloc  7507  apreap  8506  zletric  9256  zlelttric  9257  zmulcl  9265  zdceq  9287  zdcle  9288  zdclt  9289  nn0lt2  9293  elnn1uz2  9566  mnflt  9740  mnfltpnf  9742  xrltso  9753  fzdcel  9996  fzm1  10056  qletric  10200  qlelttric  10201  qdceq  10203  qsqeqor  10586  nn0o1gt2  11864  prm23lt5  12217  bj-fadc  13789  decidin  13832  triap  14061  tridceq  14088