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  3368  undif3ss  3466  reuun1  3487  prmg  3792  opthpr  3853  exmidn0m  4289  issod  4414  elelsuc  4504  ordtri2or2exmidlem  4622  regexmidlem1  4629  fununmo  5369  nndceq  6662  nndcel  6663  swoord1  6726  swoord2  6727  exmidontri2or  7454  addlocprlem  7748  msqge0  8789  mulge0  8792  ltleap  8805  nn1m1nn  9154  elnnz  9482  zletric  9516  zlelttric  9517  zmulcl  9526  zdceq  9548  zdcle  9549  zdclt  9550  ltpnf  10008  xrlttri3  10025  xrpnfdc  10070  xrmnfdc  10071  fzdcel  10268  qletric  10494  qlelttric  10495  qdceq  10497  qdclt  10498  qsqeqor  10905  hashfiv01gt1  11037  isum  11939  iprodap  12134  iprodap0  12136  nn0o1gt2  12459  prm23lt5  12829  4sqlem17  12973  gausslemma2dlem0f  15776  bj-trdc  16298  bj-nn0suc0  16495  triap  16583  tridceq  16610