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  1495  hbor  1557  nford  1578  19.30dc  1638  19.43  1639  19.32r  1691  moor  2109  r19.32r  2636  ssun1  3313  undif3ss  3411  reuun1  3432  prmg  3728  opthpr  3787  exmidn0m  4219  issod  4337  elelsuc  4427  ordtri2or2exmidlem  4543  regexmidlem1  4550  nndceq  6524  nndcel  6525  swoord1  6588  swoord2  6589  exmidontri2or  7272  addlocprlem  7564  msqge0  8603  mulge0  8606  ltleap  8619  nn1m1nn  8967  elnnz  9293  zletric  9327  zlelttric  9328  zmulcl  9336  zdceq  9358  zdcle  9359  zdclt  9360  ltpnf  9810  xrlttri3  9827  xrpnfdc  9872  xrmnfdc  9873  fzdcel  10070  qletric  10274  qlelttric  10275  qdceq  10277  qsqeqor  10662  hashfiv01gt1  10794  isum  11425  iprodap  11620  iprodap0  11622  nn0o1gt2  11942  prm23lt5  12295  4sqlem17  12439  bj-trdc  14962  bj-nn0suc0  15160  triap  15236  tridceq  15263