Theorem orc 714

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.67-2  715  pm1.4  729  orci  733  orcd  735  orcs  737  pm2.45  740  biorfi  748  pm1.5  767  pm2.4  780  pm4.44  781  pm4.78i  784  pm4.45  786  pm3.48  787  pm2.76  810  orabs  816  ordi  818  andi  820  pm4.72  829  biort  831  dcim  843  pm2.54dc  893  pm2.85dc  907  dcor  938  pm5.71dc  964  dedlema  972  3mix1  1169  xoranor  1397  19.33  1508  hbor  1570  nford  1591  19.30dc  1651  19.43  1652  19.32r  1704  moor  2126  r19.32r  2653  ssun1  3338  undif3ss  3436  reuun1  3457  prmg  3757  opthpr  3816  exmidn0m  4250  issod  4371  elelsuc  4461  ordtri2or2exmidlem  4579  regexmidlem1  4586  fununmo  5322  nndceq  6595  nndcel  6596  swoord1  6659  swoord2  6660  exmidontri2or  7368  addlocprlem  7661  msqge0  8702  mulge0  8705  ltleap  8718  nn1m1nn  9067  elnnz  9395  zletric  9429  zlelttric  9430  zmulcl  9439  zdceq  9461  zdcle  9462  zdclt  9463  ltpnf  9915  xrlttri3  9932  xrpnfdc  9977  xrmnfdc  9978  fzdcel  10175  qletric  10397  qlelttric  10398  qdceq  10400  qdclt  10401  qsqeqor  10808  hashfiv01gt1  10940  isum  11746  iprodap  11941  iprodap0  11943  nn0o1gt2  12266  prm23lt5  12636  4sqlem17  12780  gausslemma2dlem0f  15581  bj-trdc  15802  bj-nn0suc0  16000  triap  16083  tridceq  16110