Theorem orc 719

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 717	. . 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 715

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.67-2  720  pm1.4  734  orci  738  orcd  740  orcs  742  pm2.45  745  biorfi  753  pm1.5  772  pm2.4  785  pm4.44  786  pm4.78i  789  pm4.45  791  pm3.48  792  pm2.76  815  orabs  821  ordi  823  andi  825  pm4.72  834  biort  836  dcim  848  pm2.54dc  898  pm2.85dc  912  dcor  943  pm5.71dc  969  dedlema  977  3mix1  1192  xoranor  1421  19.33  1532  hbor  1594  nford  1615  19.30dc  1675  19.43  1676  19.32r  1728  moor  2151  r19.32r  2679  ssun1  3370  undif3ss  3468  reuun1  3489  prmg  3794  opthpr  3855  exmidn0m  4291  issod  4416  elelsuc  4506  ordtri2or2exmidlem  4624  regexmidlem1  4631  fununmo  5372  nndceq  6666  nndcel  6667  swoord1  6730  swoord2  6731  exmidontri2or  7460  addlocprlem  7754  msqge0  8795  mulge0  8798  ltleap  8811  nn1m1nn  9160  elnnz  9488  zletric  9522  zlelttric  9523  zmulcl  9532  zdceq  9554  zdcle  9555  zdclt  9556  ltpnf  10014  xrlttri3  10031  xrpnfdc  10076  xrmnfdc  10077  fzdcel  10274  qletric  10500  qlelttric  10501  qdceq  10503  qdclt  10504  qsqeqor  10911  hashfiv01gt1  11043  isum  11945  iprodap  12140  iprodap0  12142  nn0o1gt2  12465  prm23lt5  12835  4sqlem17  12979  gausslemma2dlem0f  15782  bj-trdc  16348  bj-nn0suc0  16545  triap  16633  tridceq  16660