Theorem orc 713

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 711	. . 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 709

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.67-2  714  pm1.4  728  orci  732  orcd  734  orcs  736  pm2.45  739  biorfi  747  pm1.5  766  pm2.4  779  pm4.44  780  pm4.78i  783  pm4.45  785  pm3.48  786  pm2.76  809  orabs  815  ordi  817  andi  819  pm4.72  828  biort  830  dcim  842  pm2.54dc  892  pm2.85dc  906  dcor  937  pm5.71dc  963  dedlema  971  3mix1  1168  xoranor  1388  19.33  1495  hbor  1557  nford  1578  19.30dc  1638  19.43  1639  19.32r  1691  moor  2113  r19.32r  2640  ssun1  3323  undif3ss  3421  reuun1  3442  prmg  3740  opthpr  3799  exmidn0m  4231  issod  4351  elelsuc  4441  ordtri2or2exmidlem  4559  regexmidlem1  4566  nndceq  6554  nndcel  6555  swoord1  6618  swoord2  6619  exmidontri2or  7305  addlocprlem  7597  msqge0  8637  mulge0  8640  ltleap  8653  nn1m1nn  9002  elnnz  9330  zletric  9364  zlelttric  9365  zmulcl  9373  zdceq  9395  zdcle  9396  zdclt  9397  ltpnf  9849  xrlttri3  9866  xrpnfdc  9911  xrmnfdc  9912  fzdcel  10109  qletric  10314  qlelttric  10315  qdceq  10317  qdclt  10318  qsqeqor  10724  hashfiv01gt1  10856  isum  11531  iprodap  11726  iprodap0  11728  nn0o1gt2  12049  prm23lt5  12404  4sqlem17  12548  gausslemma2dlem0f  15211  bj-trdc  15314  bj-nn0suc0  15512  triap  15589  tridceq  15616