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	⊢ (𝜑 → (𝜑 ∨ 𝜓))

Proof of Theorem orc

Step	Hyp	Ref	Expression
1		id 19	. . 3 ⊢ ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜓))
2		jaob 711	. . 3 ⊢ (((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜓)) ↔ ((𝜑 → (𝜑 ∨ 𝜓)) ∧ (𝜓 → (𝜑 ∨ 𝜓))))
3	1, 2	mpbi 145	. 2 ⊢ ((𝜑 → (𝜑 ∨ 𝜓)) ∧ (𝜓 → (𝜑 ∨ 𝜓)))
4	3	simpli 111	1 ⊢ (𝜑 → (𝜑 ∨ 𝜓))

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  3327  undif3ss  3425  reuun1  3446  prmg  3744  opthpr  3803  exmidn0m  4235  issod  4355  elelsuc  4445  ordtri2or2exmidlem  4563  regexmidlem1  4570  nndceq  6566  nndcel  6567  swoord1  6630  swoord2  6631  exmidontri2or  7328  addlocprlem  7621  msqge0  8662  mulge0  8665  ltleap  8678  nn1m1nn  9027  elnnz  9355  zletric  9389  zlelttric  9390  zmulcl  9398  zdceq  9420  zdcle  9421  zdclt  9422  ltpnf  9874  xrlttri3  9891  xrpnfdc  9936  xrmnfdc  9937  fzdcel  10134  qletric  10350  qlelttric  10351  qdceq  10353  qdclt  10354  qsqeqor  10761  hashfiv01gt1  10893  isum  11569  iprodap  11764  iprodap0  11766  nn0o1gt2  12089  prm23lt5  12459  4sqlem17  12603  gausslemma2dlem0f  15403  bj-trdc  15506  bj-nn0suc0  15704  triap  15786  tridceq  15813