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

Proof of Theorem orc

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

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  3833  opthpr  3895  exmidn0m  4336  issod  4462  elelsuc  4552  ordtri2or2exmidlem  4671  regexmidlem1  4678  fununmo  5421  nndceq  6766  nndcel  6767  swoord1  6830  swoord2  6831  exmidontri2or  7596  addlocprlem  7896  msqge0  8938  mulge0  8941  ltleap  8954  nn1m1nn  9305  elnnz  9637  zletric  9671  zlelttric  9672  zmulcl  9681  zdceq  9703  zdcle  9704  zdclt  9705  ltpnf  10165  xrlttri3  10182  xrpnfdc  10227  xrmnfdc  10228  fzdcel  10427  qletric  10659  qlelttric  10660  qdceq  10662  qdclt  10663  qsqeqor  11070  hashfiv01gt1  11204  isum  12135  iprodap  12330  iprodap0  12332  nn0o1gt2  12655  prm23lt5  13025  4sqlem17  13169  gausslemma2dlem0f  16156  bj-trdc  16763  bj-nn0suc0  16959  triap  17052  tridceq  17080