Theorem orc 713

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 711	. . 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 709

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.67-2  714  pm1.4  728  orci  732  orcd  734  orcs  736  pm2.45  739  biorfi  747  pm1.5  766  pm2.4  779  pm4.44  780  pm4.78i  783  pm4.45  785  pm3.48  786  pm2.76  809  orabs  815  ordi  817  andi  819  pm4.72  828  biort  830  dcim  842  pm2.54dc  892  pm2.85dc  906  dcor  937  pm5.71dc  963  dedlema  971  3mix1  1168  xoranor  1388  19.33  1498  hbor  1560  nford  1581  19.30dc  1641  19.43  1642  19.32r  1694  moor  2116  r19.32r  2643  ssun1  3326  undif3ss  3424  reuun1  3445  prmg  3743  opthpr  3802  exmidn0m  4234  issod  4354  elelsuc  4444  ordtri2or2exmidlem  4562  regexmidlem1  4569  nndceq  6557  nndcel  6558  swoord1  6621  swoord2  6622  exmidontri2or  7310  addlocprlem  7602  msqge0  8643  mulge0  8646  ltleap  8659  nn1m1nn  9008  elnnz  9336  zletric  9370  zlelttric  9371  zmulcl  9379  zdceq  9401  zdcle  9402  zdclt  9403  ltpnf  9855  xrlttri3  9872  xrpnfdc  9917  xrmnfdc  9918  fzdcel  10115  qletric  10331  qlelttric  10332  qdceq  10334  qdclt  10335  qsqeqor  10742  hashfiv01gt1  10874  isum  11550  iprodap  11745  iprodap0  11747  nn0o1gt2  12070  prm23lt5  12432  4sqlem17  12576  gausslemma2dlem0f  15295  bj-trdc  15398  bj-nn0suc0  15596  triap  15673  tridceq  15700