Theorem orc 701

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 699	. . 3 |- ( ( ( ph \/ ps ) -> ( ph \/ ps ) ) <-> ( ( ph -> ( ph \/ ps ) ) /\ ( ps -> ( ph \/ ps ) ) ) )
3	1, 2	mpbi 144	. 2 |- ( ( ph -> ( ph \/ ps ) ) /\ ( ps -> ( ph \/ ps ) ) )
4	3	simpli 110	1 |- ( ph -> ( ph \/ ps ) )

Syntax hints:   -> wi 4   /\ wa 103   \/ wo 697

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm2.67-2  702  pm1.4  716  orci  720  orcd  722  orcs  724  pm2.45  727  biorfi  735  pm1.5  754  pm2.4  767  pm4.44  768  pm4.78i  771  pm4.45  773  pm3.48  774  pm2.76  797  orabs  803  ordi  805  andi  807  pm4.72  812  biort  814  dcim  826  pm2.54dc  876  pm2.85dc  890  dcor  919  pm5.71dc  945  dedlema  953  3mix1  1150  xoranor  1355  19.33  1460  hbor  1525  nford  1546  19.30dc  1606  19.43  1607  19.32r  1658  moor  2068  r19.32r  2576  ssun1  3234  undif3ss  3332  reuun1  3353  prmg  3639  opthpr  3694  exmidn0m  4119  issod  4236  elelsuc  4326  ordtri2or2exmidlem  4436  regexmidlem1  4443  nndceq  6388  nndcel  6389  swoord1  6451  swoord2  6452  addlocprlem  7336  msqge0  8371  mulge0  8374  ltleap  8387  nn1m1nn  8731  elnnz  9057  zletric  9091  zlelttric  9092  zmulcl  9100  zdceq  9119  zdcle  9120  zdclt  9121  ltpnf  9560  xrlttri3  9576  xrpnfdc  9618  xrmnfdc  9619  fzdcel  9813  qletric  10014  qlelttric  10015  qdceq  10017  hashfiv01gt1  10521  isum  11147  nn0o1gt2  11591  bj-trdc  12948  bj-nn0suc0  13137  triap  13213