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  1727  moor  2150  r19.32r  2678  ssun1  3369  undif3ss  3467  reuun1  3488  prmg  3793  opthpr  3854  exmidn0m  4290  issod  4415  elelsuc  4505  ordtri2or2exmidlem  4623  regexmidlem1  4630  fununmo  5371  nndceq  6669  nndcel  6670  swoord1  6733  swoord2  6734  exmidontri2or  7463  addlocprlem  7757  msqge0  8798  mulge0  8801  ltleap  8814  nn1m1nn  9163  elnnz  9491  zletric  9525  zlelttric  9526  zmulcl  9535  zdceq  9557  zdcle  9558  zdclt  9559  ltpnf  10017  xrlttri3  10034  xrpnfdc  10079  xrmnfdc  10080  fzdcel  10277  qletric  10504  qlelttric  10505  qdceq  10507  qdclt  10508  qsqeqor  10915  hashfiv01gt1  11047  isum  11966  iprodap  12161  iprodap0  12163  nn0o1gt2  12486  prm23lt5  12856  4sqlem17  13000  gausslemma2dlem0f  15809  bj-trdc  16406  bj-nn0suc0  16603  triap  16695  tridceq  16723