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  3298  undif3ss  3396  reuun1  3417  prmg  3713  opthpr  3771  exmidn0m  4199  issod  4317  elelsuc  4407  ordtri2or2exmidlem  4523  regexmidlem1  4530  nndceq  6495  nndcel  6496  swoord1  6559  swoord2  6560  exmidontri2or  7237  addlocprlem  7529  msqge0  8567  mulge0  8570  ltleap  8583  nn1m1nn  8931  elnnz  9257  zletric  9291  zlelttric  9292  zmulcl  9300  zdceq  9322  zdcle  9323  zdclt  9324  ltpnf  9774  xrlttri3  9791  xrpnfdc  9836  xrmnfdc  9837  fzdcel  10033  qletric  10237  qlelttric  10238  qdceq  10240  qsqeqor  10623  hashfiv01gt1  10753  isum  11384  iprodap  11579  iprodap0  11581  nn0o1gt2  11900  prm23lt5  12253  bj-trdc  14275  bj-nn0suc0  14473  triap  14548  tridceq  14575