Theorem orc 720

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 718	. . 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 716

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.67-2  721  pm1.4  735  orci  739  orcd  741  orcs  743  pm2.45  746  biorfi  754  pm1.5  773  pm2.4  786  pm4.44  787  pm4.78i  790  pm4.45  792  pm3.48  793  pm2.76  816  orabs  822  ordi  824  andi  826  pm4.72  835  biort  837  dcim  849  pm2.54dc  899  pm2.85dc  913  dcor  944  pm5.71dc  970  dedlema  978  3mix1  1193  xoranor  1422  19.33  1533  hbor  1595  nford  1616  19.30dc  1676  19.43  1677  19.32r  1728  moor  2151  r19.32r  2680  ssun1  3372  undif3ss  3470  reuun1  3491  prmg  3798  opthpr  3860  exmidn0m  4297  issod  4422  elelsuc  4512  ordtri2or2exmidlem  4630  regexmidlem1  4637  fununmo  5379  nndceq  6710  nndcel  6711  swoord1  6774  swoord2  6775  exmidontri2or  7504  addlocprlem  7798  msqge0  8838  mulge0  8841  ltleap  8854  nn1m1nn  9203  elnnz  9533  zletric  9567  zlelttric  9568  zmulcl  9577  zdceq  9599  zdcle  9600  zdclt  9601  ltpnf  10059  xrlttri3  10076  xrpnfdc  10121  xrmnfdc  10122  fzdcel  10320  qletric  10547  qlelttric  10548  qdceq  10550  qdclt  10551  qsqeqor  10958  hashfiv01gt1  11090  isum  12009  iprodap  12204  iprodap0  12206  nn0o1gt2  12529  prm23lt5  12899  4sqlem17  13043  gausslemma2dlem0f  15856  bj-trdc  16453  bj-nn0suc0  16649  triap  16744  tridceq  16772