Theorem orc 720

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.67-2  721  pm1.4  735  orci  739  orcd  741  orcs  743  pm2.45  746  biorfi  754  pm1.5  773  pm2.4  786  pm4.44  787  pm4.78i  790  pm4.45  792  pm3.48  793  pm2.76  816  orabs  822  ordi  824  andi  826  pm4.72  835  biort  837  dcim  849  pm2.54dc  899  pm2.85dc  913  dcor  944  pm5.71dc  970  dedlema  978  3mix1  1193  xoranor  1422  19.33  1533  hbor  1595  nford  1616  19.30dc  1676  19.43  1677  19.32r  1728  moor  2152  r19.32r  2689  ssun1  3381  undif3ss  3481  reuun1  3502  prmg  3813  opthpr  3875  exmidn0m  4313  issod  4439  elelsuc  4529  ordtri2or2exmidlem  4647  regexmidlem1  4654  fununmo  5397  nndceq  6731  nndcel  6732  swoord1  6795  swoord2  6796  exmidontri2or  7552  addlocprlem  7849  msqge0  8889  mulge0  8892  ltleap  8905  nn1m1nn  9254  elnnz  9586  zletric  9620  zlelttric  9621  zmulcl  9630  zdceq  9652  zdcle  9653  zdclt  9654  ltpnf  10112  xrlttri3  10129  xrpnfdc  10174  xrmnfdc  10175  fzdcel  10373  qletric  10600  qlelttric  10601  qdceq  10603  qdclt  10604  qsqeqor  11011  hashfiv01gt1  11143  isum  12067  iprodap  12262  iprodap0  12264  nn0o1gt2  12587  prm23lt5  12957  4sqlem17  13101  gausslemma2dlem0f  15919  bj-trdc  16516  bj-nn0suc0  16712  triap  16805  tridceq  16833