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  2154  r19.32r  2691  ssun1  3386  undif3ss  3486  reuun1  3507  prmg  3819  opthpr  3881  exmidn0m  4319  issod  4445  elelsuc  4535  ordtri2or2exmidlem  4653  regexmidlem1  4660  fununmo  5403  nndceq  6745  nndcel  6746  swoord1  6809  swoord2  6810  exmidontri2or  7566  addlocprlem  7866  msqge0  8907  mulge0  8910  ltleap  8923  nn1m1nn  9272  elnnz  9604  zletric  9638  zlelttric  9639  zmulcl  9648  zdceq  9670  zdcle  9671  zdclt  9672  ltpnf  10132  xrlttri3  10149  xrpnfdc  10194  xrmnfdc  10195  fzdcel  10394  qletric  10625  qlelttric  10626  qdceq  10628  qdclt  10629  qsqeqor  11036  hashfiv01gt1  11170  isum  12096  iprodap  12291  iprodap0  12293  nn0o1gt2  12616  prm23lt5  12986  4sqlem17  13130  gausslemma2dlem0f  16039  bj-trdc  16636  bj-nn0suc0  16832  triap  16925  tridceq  16953