Theorem orc 717

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 715	. . 3 ⊢ (((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜓)) ↔ ((𝜑 → (𝜑 ∨ 𝜓)) ∧ (𝜓 → (𝜑 ∨ 𝜓))))
3	1, 2	mpbi 145	. 2 ⊢ ((𝜑 → (𝜑 ∨ 𝜓)) ∧ (𝜓 → (𝜑 ∨ 𝜓)))
4	3	simpli 111	1 ⊢ (𝜑 → (𝜑 ∨ 𝜓))

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 713

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.67-2  718  pm1.4  732  orci  736  orcd  738  orcs  740  pm2.45  743  biorfi  751  pm1.5  770  pm2.4  783  pm4.44  784  pm4.78i  787  pm4.45  789  pm3.48  790  pm2.76  813  orabs  819  ordi  821  andi  823  pm4.72  832  biort  834  dcim  846  pm2.54dc  896  pm2.85dc  910  dcor  941  pm5.71dc  967  dedlema  975  3mix1  1190  xoranor  1419  19.33  1530  hbor  1592  nford  1613  19.30dc  1673  19.43  1674  19.32r  1726  moor  2149  r19.32r  2677  ssun1  3367  undif3ss  3465  reuun1  3486  prmg  3788  opthpr  3849  exmidn0m  4284  issod  4407  elelsuc  4497  ordtri2or2exmidlem  4615  regexmidlem1  4622  fununmo  5359  nndceq  6635  nndcel  6636  swoord1  6699  swoord2  6700  exmidontri2or  7416  addlocprlem  7710  msqge0  8751  mulge0  8754  ltleap  8767  nn1m1nn  9116  elnnz  9444  zletric  9478  zlelttric  9479  zmulcl  9488  zdceq  9510  zdcle  9511  zdclt  9512  ltpnf  9964  xrlttri3  9981  xrpnfdc  10026  xrmnfdc  10027  fzdcel  10224  qletric  10448  qlelttric  10449  qdceq  10451  qdclt  10452  qsqeqor  10859  hashfiv01gt1  10991  isum  11882  iprodap  12077  iprodap0  12079  nn0o1gt2  12402  prm23lt5  12772  4sqlem17  12916  gausslemma2dlem0f  15718  bj-trdc  16046  bj-nn0suc0  16243  triap  16328  tridceq  16355