Theorem orc 724

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 722	. . 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 720

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.67-2  725  pm1.4  739  orci  743  orcd  745  orcs  747  pm2.45  750  biorfi  758  pm1.5  777  pm2.4  790  pm4.44  791  pm4.78i  794  pm4.45  796  pm3.48  797  pm2.76  820  orabs  826  ordi  828  andi  830  pm4.72  839  biort  841  dcim  853  pm2.54dc  903  pm2.85dc  917  dcor  948  pm5.71dc  974  dedlema  982  3mix1  1197  xoranor  1426  19.33  1537  hbor  1599  nford  1620  19.30dc  1680  19.43  1681  19.32r  1732  moor  2158  r19.32r  2697  ssun1  3392  undif3ss  3492  reuun1  3515  prmg  3830  opthpr  3892  exmidn0m  4333  issod  4459  elelsuc  4549  ordtri2or2exmidlem  4668  regexmidlem1  4675  fununmo  5418  nndceq  6762  nndcel  6763  swoord1  6826  swoord2  6827  exmidontri2or  7592  addlocprlem  7892  msqge0  8934  mulge0  8937  ltleap  8950  nn1m1nn  9301  elnnz  9633  zletric  9667  zlelttric  9668  zmulcl  9677  zdceq  9699  zdcle  9700  zdclt  9701  ltpnf  10161  xrlttri3  10178  xrpnfdc  10223  xrmnfdc  10224  fzdcel  10423  qletric  10654  qlelttric  10655  qdceq  10657  qdclt  10658  qsqeqor  11065  hashfiv01gt1  11199  isum  12130  iprodap  12325  iprodap0  12327  nn0o1gt2  12650  prm23lt5  13020  4sqlem17  13164  gausslemma2dlem0f  16087  bj-trdc  16694  bj-nn0suc0  16890  triap  16983  tridceq  17011