Theorem orc 720

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.67-2  721  pm1.4  735  orci  739  orcd  741  orcs  743  pm2.45  746  biorfi  754  pm1.5  773  pm2.4  786  pm4.44  787  pm4.78i  790  pm4.45  792  pm3.48  793  pm2.76  816  orabs  822  ordi  824  andi  826  pm4.72  835  biort  837  dcim  849  pm2.54dc  899  pm2.85dc  913  dcor  944  pm5.71dc  970  dedlema  978  3mix1  1193  xoranor  1422  19.33  1533  hbor  1595  nford  1616  19.30dc  1676  19.43  1677  19.32r  1728  moor  2152  r19.32r  2689  ssun1  3382  undif3ss  3482  reuun1  3503  prmg  3814  opthpr  3876  exmidn0m  4314  issod  4440  elelsuc  4530  ordtri2or2exmidlem  4648  regexmidlem1  4655  fununmo  5398  nndceq  6732  nndcel  6733  swoord1  6796  swoord2  6797  exmidontri2or  7553  addlocprlem  7850  msqge0  8890  mulge0  8893  ltleap  8906  nn1m1nn  9255  elnnz  9587  zletric  9621  zlelttric  9622  zmulcl  9631  zdceq  9653  zdcle  9654  zdclt  9655  ltpnf  10113  xrlttri3  10130  xrpnfdc  10175  xrmnfdc  10176  fzdcel  10374  qletric  10601  qlelttric  10602  qdceq  10604  qdclt  10605  qsqeqor  11012  hashfiv01gt1  11145  isum  12071  iprodap  12266  iprodap0  12268  nn0o1gt2  12591  prm23lt5  12961  4sqlem17  13105  gausslemma2dlem0f  15927  bj-trdc  16524  bj-nn0suc0  16720  triap  16813  tridceq  16841