Theorem orc 713

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 711	. . 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 709

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.67-2  714  pm1.4  728  orci  732  orcd  734  orcs  736  pm2.45  739  biorfi  747  pm1.5  766  pm2.4  779  pm4.44  780  pm4.78i  783  pm4.45  785  pm3.48  786  pm2.76  809  orabs  815  ordi  817  andi  819  pm4.72  828  biort  830  dcim  842  pm2.54dc  892  pm2.85dc  906  dcor  937  pm5.71dc  963  dedlema  971  3mix1  1168  xoranor  1388  19.33  1498  hbor  1560  nford  1581  19.30dc  1641  19.43  1642  19.32r  1694  moor  2116  r19.32r  2643  ssun1  3327  undif3ss  3425  reuun1  3446  prmg  3744  opthpr  3803  exmidn0m  4235  issod  4355  elelsuc  4445  ordtri2or2exmidlem  4563  regexmidlem1  4570  nndceq  6566  nndcel  6567  swoord1  6630  swoord2  6631  exmidontri2or  7326  addlocprlem  7619  msqge0  8660  mulge0  8663  ltleap  8676  nn1m1nn  9025  elnnz  9353  zletric  9387  zlelttric  9388  zmulcl  9396  zdceq  9418  zdcle  9419  zdclt  9420  ltpnf  9872  xrlttri3  9889  xrpnfdc  9934  xrmnfdc  9935  fzdcel  10132  qletric  10348  qlelttric  10349  qdceq  10351  qdclt  10352  qsqeqor  10759  hashfiv01gt1  10891  isum  11567  iprodap  11762  iprodap0  11764  nn0o1gt2  12087  prm23lt5  12457  4sqlem17  12601  gausslemma2dlem0f  15379  bj-trdc  15482  bj-nn0suc0  15680  triap  15760  tridceq  15787