Theorem orc 714

Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.)

Assertion

Ref	Expression
orc	|- ( ph -> ( ph \/ ps ) )

Proof of Theorem orc

Step	Hyp	Ref	Expression
1		id 19	. . 3 |- ( ( ph \/ ps ) -> ( ph \/ ps ) )
2		jaob 712	. . 3 |- ( ( ( ph \/ ps ) -> ( ph \/ ps ) ) <-> ( ( ph -> ( ph \/ ps ) ) /\ ( ps -> ( ph \/ ps ) ) ) )
3	1, 2	mpbi 145	. 2 |- ( ( ph -> ( ph \/ ps ) ) /\ ( ps -> ( ph \/ ps ) ) )
4	3	simpli 111	1 |- ( ph -> ( ph \/ ps ) )

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 710

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.67-2  715  pm1.4  729  orci  733  orcd  735  orcs  737  pm2.45  740  biorfi  748  pm1.5  767  pm2.4  780  pm4.44  781  pm4.78i  784  pm4.45  786  pm3.48  787  pm2.76  810  orabs  816  ordi  818  andi  820  pm4.72  829  biort  831  dcim  843  pm2.54dc  893  pm2.85dc  907  dcor  938  pm5.71dc  964  dedlema  972  3mix1  1169  xoranor  1397  19.33  1508  hbor  1570  nford  1591  19.30dc  1651  19.43  1652  19.32r  1704  moor  2127  r19.32r  2654  ssun1  3344  undif3ss  3442  reuun1  3463  prmg  3765  opthpr  3826  exmidn0m  4261  issod  4384  elelsuc  4474  ordtri2or2exmidlem  4592  regexmidlem1  4599  fununmo  5335  nndceq  6608  nndcel  6609  swoord1  6672  swoord2  6673  exmidontri2or  7389  addlocprlem  7683  msqge0  8724  mulge0  8727  ltleap  8740  nn1m1nn  9089  elnnz  9417  zletric  9451  zlelttric  9452  zmulcl  9461  zdceq  9483  zdcle  9484  zdclt  9485  ltpnf  9937  xrlttri3  9954  xrpnfdc  9999  xrmnfdc  10000  fzdcel  10197  qletric  10421  qlelttric  10422  qdceq  10424  qdclt  10425  qsqeqor  10832  hashfiv01gt1  10964  isum  11811  iprodap  12006  iprodap0  12008  nn0o1gt2  12331  prm23lt5  12701  4sqlem17  12845  gausslemma2dlem0f  15646  bj-trdc  15888  bj-nn0suc0  16085  triap  16170  tridceq  16197