Theorem orc 702

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 700	. . 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 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm2.67-2  703  pm1.4  717  orci  721  orcd  723  orcs  725  pm2.45  728  biorfi  736  pm1.5  755  pm2.4  768  pm4.44  769  pm4.78i  772  pm4.45  774  pm3.48  775  pm2.76  798  orabs  804  ordi  806  andi  808  pm4.72  817  biort  819  dcim  831  pm2.54dc  881  pm2.85dc  895  dcor  925  pm5.71dc  951  dedlema  959  3mix1  1156  xoranor  1367  19.33  1472  hbor  1534  nford  1555  19.30dc  1615  19.43  1616  19.32r  1668  moor  2085  r19.32r  2611  ssun1  3284  undif3ss  3382  reuun1  3403  prmg  3696  opthpr  3751  exmidn0m  4179  issod  4296  elelsuc  4386  ordtri2or2exmidlem  4502  regexmidlem1  4509  nndceq  6463  nndcel  6464  swoord1  6526  swoord2  6527  exmidontri2or  7195  addlocprlem  7472  msqge0  8510  mulge0  8513  ltleap  8526  nn1m1nn  8871  elnnz  9197  zletric  9231  zlelttric  9232  zmulcl  9240  zdceq  9262  zdcle  9263  zdclt  9264  ltpnf  9712  xrlttri3  9729  xrpnfdc  9774  xrmnfdc  9775  fzdcel  9971  qletric  10175  qlelttric  10176  qdceq  10178  qsqeqor  10561  hashfiv01gt1  10691  isum  11322  iprodap  11517  iprodap0  11519  nn0o1gt2  11838  prm23lt5  12191  bj-trdc  13593  bj-nn0suc0  13792  triap  13868  tridceq  13895