Theorem orc 712

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.67-2  713  pm1.4  727  orci  731  orcd  733  orcs  735  pm2.45  738  biorfi  746  pm1.5  765  pm2.4  778  pm4.44  779  pm4.78i  782  pm4.45  784  pm3.48  785  pm2.76  808  orabs  814  ordi  816  andi  818  pm4.72  827  biort  829  dcim  841  pm2.54dc  891  pm2.85dc  905  dcor  935  pm5.71dc  961  dedlema  969  3mix1  1166  xoranor  1377  19.33  1484  hbor  1546  nford  1567  19.30dc  1627  19.43  1628  19.32r  1680  moor  2097  r19.32r  2623  ssun1  3299  undif3ss  3397  reuun1  3418  prmg  3714  opthpr  3773  exmidn0m  4202  issod  4320  elelsuc  4410  ordtri2or2exmidlem  4526  regexmidlem1  4533  nndceq  6500  nndcel  6501  swoord1  6564  swoord2  6565  exmidontri2or  7242  addlocprlem  7534  msqge0  8573  mulge0  8576  ltleap  8589  nn1m1nn  8937  elnnz  9263  zletric  9297  zlelttric  9298  zmulcl  9306  zdceq  9328  zdcle  9329  zdclt  9330  ltpnf  9780  xrlttri3  9797  xrpnfdc  9842  xrmnfdc  9843  fzdcel  10040  qletric  10244  qlelttric  10245  qdceq  10247  qsqeqor  10631  hashfiv01gt1  10762  isum  11393  iprodap  11588  iprodap0  11590  nn0o1gt2  11910  prm23lt5  12263  bj-trdc  14507  bj-nn0suc0  14705  triap  14780  tridceq  14807