Theorem orc 665

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 663	. . 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 661

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm2.67-2  666  pm1.4  678  orci  682  orcd  684  orcs  686  pm2.45  689  biorfi  697  pm1.5  714  pm2.4  727  pm4.44  728  pm4.45  730  pm3.48  731  pm2.76  754  orabs  760  ordi  762  andi  764  pm4.72  769  biort  771  dcim  817  pm2.54dc  823  pm4.78i  841  pm2.85dc  844  dcor  876  pm5.71dc  902  dedlema  910  3mix1  1107  xoranor  1308  19.33  1413  hbor  1478  nford  1499  19.30dc  1558  19.43  1559  19.32r  1610  moor  2012  r19.32r  2501  ssun1  3135  undif3ss  3225  reuun1  3246  prmg  3511  opthpr  3564  issod  4074  elelsuc  4164  ordtri2or2exmidlem  4269  regexmidlem1  4276  nndceq  6100  nndcel  6101  swoord1  6158  swoord2  6159  addlocprlem  6725  msqge0  7716  mulge0  7719  ltleap  7730  nn1m1nn  8057  elnnz  8361  zletric  8395  zlelttric  8396  zmulcl  8404  zdceq  8423  zdcle  8424  zdclt  8425  ltpnf  8856  xrlttri3  8872  fzdcel  9059  qletric  9253  qlelttric  9254  qdceq  9256  nn0o1gt2  10305  bj-nn0suc0  10745