Theorem orc 714

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 712	. . 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 710

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.67-2  715  pm1.4  729  orci  733  orcd  735  orcs  737  pm2.45  740  biorfi  748  pm1.5  767  pm2.4  780  pm4.44  781  pm4.78i  784  pm4.45  786  pm3.48  787  pm2.76  810  orabs  816  ordi  818  andi  820  pm4.72  829  biort  831  dcim  843  pm2.54dc  893  pm2.85dc  907  dcor  938  pm5.71dc  964  dedlema  972  3mix1  1169  xoranor  1397  19.33  1507  hbor  1569  nford  1590  19.30dc  1650  19.43  1651  19.32r  1703  moor  2125  r19.32r  2652  ssun1  3336  undif3ss  3434  reuun1  3455  prmg  3754  opthpr  3813  exmidn0m  4245  issod  4366  elelsuc  4456  ordtri2or2exmidlem  4574  regexmidlem1  4581  fununmo  5316  nndceq  6585  nndcel  6586  swoord1  6649  swoord2  6650  exmidontri2or  7355  addlocprlem  7648  msqge0  8689  mulge0  8692  ltleap  8705  nn1m1nn  9054  elnnz  9382  zletric  9416  zlelttric  9417  zmulcl  9426  zdceq  9448  zdcle  9449  zdclt  9450  ltpnf  9902  xrlttri3  9919  xrpnfdc  9964  xrmnfdc  9965  fzdcel  10162  qletric  10384  qlelttric  10385  qdceq  10387  qdclt  10388  qsqeqor  10795  hashfiv01gt1  10927  isum  11696  iprodap  11891  iprodap0  11893  nn0o1gt2  12216  prm23lt5  12586  4sqlem17  12730  gausslemma2dlem0f  15531  bj-trdc  15688  bj-nn0suc0  15886  triap  15968  tridceq  15995