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  2113  r19.32r  2640  ssun1  3322  undif3ss  3420  reuun1  3441  prmg  3739  opthpr  3798  exmidn0m  4230  issod  4350  elelsuc  4440  ordtri2or2exmidlem  4558  regexmidlem1  4565  nndceq  6552  nndcel  6553  swoord1  6616  swoord2  6617  exmidontri2or  7303  addlocprlem  7595  msqge0  8635  mulge0  8638  ltleap  8651  nn1m1nn  9000  elnnz  9327  zletric  9361  zlelttric  9362  zmulcl  9370  zdceq  9392  zdcle  9393  zdclt  9394  ltpnf  9846  xrlttri3  9863  xrpnfdc  9908  xrmnfdc  9909  fzdcel  10106  qletric  10311  qlelttric  10312  qdceq  10314  qdclt  10315  qsqeqor  10721  hashfiv01gt1  10853  isum  11528  iprodap  11723  iprodap0  11725  nn0o1gt2  12046  prm23lt5  12401  4sqlem17  12545  gausslemma2dlem0f  15170  bj-trdc  15244  bj-nn0suc0  15442  triap  15519  tridceq  15546