Theorem olc 701

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 700	. . 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 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  oibabs  704  pm1.4  717  olci  722  pm2.07  727  pm2.46  729  biorf  734  pm1.5  755  pm2.41  766  pm4.78i  772  pm3.48  775  ordi  806  andi  808  pm4.72  817  stdcn  837  pm2.54dc  881  pm2.85dc  895  dcor  925  dedlemb  960  xoranor  1367  19.33  1472  hbor  1534  nford  1555  19.30dc  1615  19.43  1616  19.32r  1668  euor2  2072  mooran2  2087  r19.32r  2612  undif3ss  3383  undif4  3471  issod  4297  onsucelsucexmid  4507  sucprcreg  4526  0elnn  4596  acexmidlemph  5835  nntri3or  6461  swoord1  6530  swoord2  6531  exmidaclem  7164  exmidontri2or  7199  addlocprlem  7476  nqprloc  7486  apreap  8485  zletric  9235  zlelttric  9236  zmulcl  9244  zdceq  9266  zdcle  9267  zdclt  9268  nn0lt2  9272  elnn1uz2  9545  mnflt  9719  mnfltpnf  9721  xrltso  9732  fzdcel  9975  fzm1  10035  qletric  10179  qlelttric  10180  qdceq  10182  qsqeqor  10565  nn0o1gt2  11842  prm23lt5  12195  bj-fadc  13635  decidin  13678  triap  13908  tridceq  13935