Theorem orc 666

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 664	. . 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 662

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm2.67-2  667  pm1.4  679  orci  683  orcd  685  orcs  687  pm2.45  690  biorfi  698  pm1.5  715  pm2.4  728  pm4.44  729  pm4.45  731  pm3.48  732  pm2.76  755  orabs  761  ordi  763  andi  765  pm4.72  770  biort  772  dcim  818  pm2.54dc  824  pm4.78i  842  pm2.85dc  845  dcor  877  pm5.71dc  903  dedlema  911  3mix1  1108  xoranor  1309  19.33  1414  hbor  1479  nford  1500  19.30dc  1559  19.43  1560  19.32r  1611  moor  2013  r19.32r  2502  ssun1  3136  undif3ss  3232  reuun1  3253  prmg  3519  opthpr  3572  issod  4082  elelsuc  4172  ordtri2or2exmidlem  4277  regexmidlem1  4284  nndceq  6143  nndcel  6144  swoord1  6201  swoord2  6202  addlocprlem  6787  msqge0  7783  mulge0  7786  ltleap  7797  nn1m1nn  8124  elnnz  8442  zletric  8476  zlelttric  8477  zmulcl  8485  zdceq  8504  zdcle  8505  zdclt  8506  ltpnf  8932  xrlttri3  8948  fzdcel  9135  qletric  9330  qlelttric  9331  qdceq  9333  sizefiv01gt1  9806  nn0o1gt2  10449  bj-nn0suc0  10903