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  2151  r19.32r  2680  ssun1  3372  undif3ss  3470  reuun1  3491  prmg  3798  opthpr  3860  exmidn0m  4297  issod  4422  elelsuc  4512  ordtri2or2exmidlem  4630  regexmidlem1  4637  fununmo  5379  nndceq  6710  nndcel  6711  swoord1  6774  swoord2  6775  exmidontri2or  7504  addlocprlem  7798  msqge0  8839  mulge0  8842  ltleap  8855  nn1m1nn  9204  elnnz  9532  zletric  9566  zlelttric  9567  zmulcl  9576  zdceq  9598  zdcle  9599  zdclt  9600  ltpnf  10058  xrlttri3  10075  xrpnfdc  10120  xrmnfdc  10121  fzdcel  10318  qletric  10545  qlelttric  10546  qdceq  10548  qdclt  10549  qsqeqor  10956  hashfiv01gt1  11088  isum  12007  iprodap  12202  iprodap0  12204  nn0o1gt2  12527  prm23lt5  12897  4sqlem17  13041  gausslemma2dlem0f  15853  bj-trdc  16450  bj-nn0suc0  16646  triap  16741  tridceq  16769