Theorem orc 668

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 666	. . 3 |- ( ( ( ph \/ ps ) -> ( ph \/ ps ) ) <-> ( ( ph -> ( ph \/ ps ) ) /\ ( ps -> ( ph \/ ps ) ) ) )
3	1, 2	mpbi 143	. 2 |- ( ( ph -> ( ph \/ ps ) ) /\ ( ps -> ( ph \/ ps ) ) )
4	3	simpli 109	1 |- ( ph -> ( ph \/ ps ) )

Syntax hints:   -> wi 4   /\ wa 102   \/ wo 664

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm2.67-2  669  pm1.4  681  orci  685  orcd  687  orcs  689  pm2.45  692  biorfi  700  pm1.5  717  pm2.4  730  pm4.44  731  pm4.45  733  pm3.48  734  pm2.76  757  orabs  763  ordi  765  andi  767  pm4.72  772  biort  774  dcim  822  pm2.54dc  828  pm4.78i  846  pm2.85dc  849  dcor  881  pm5.71dc  907  dedlema  915  3mix1  1112  xoranor  1313  19.33  1418  hbor  1483  nford  1504  19.30dc  1563  19.43  1564  19.32r  1615  moor  2019  r19.32r  2514  ssun1  3163  undif3ss  3260  reuun1  3281  prmg  3561  opthpr  3616  issod  4146  elelsuc  4236  ordtri2or2exmidlem  4342  regexmidlem1  4349  nndceq  6260  nndcel  6261  swoord1  6321  swoord2  6322  addlocprlem  7094  msqge0  8093  mulge0  8096  ltleap  8107  nn1m1nn  8440  elnnz  8760  zletric  8794  zlelttric  8795  zmulcl  8803  zdceq  8822  zdcle  8823  zdclt  8824  ltpnf  9251  xrlttri3  9267  fzdcel  9454  qletric  9655  qlelttric  9656  qdceq  9658  hashfiv01gt1  10190  iisum  10775  nn0o1gt2  11183  bj-nn0suc0  11845