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  8908  mulge0  8911  ltleap  8924  nn1m1nn  9275  elnnz  9607  zletric  9641  zlelttric  9642  zmulcl  9651  zdceq  9673  zdcle  9674  zdclt  9675  ltpnf  10135  xrlttri3  10152  xrpnfdc  10197  xrmnfdc  10198  fzdcel  10397  qletric  10628  qlelttric  10629  qdceq  10631  qdclt  10632  qsqeqor  11039  hashfiv01gt1  11173  isum  12100  iprodap  12295  iprodap0  12297  nn0o1gt2  12620  prm23lt5  12990  4sqlem17  13134  gausslemma2dlem0f  16057  bj-trdc  16664  bj-nn0suc0  16860  triap  16953  tridceq  16981