Theorem orc 724

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm2.67-2  725  pm1.4  739  orci  743  orcd  745  orcs  747  pm2.45  750  biorfi  758  pm1.5  777  pm2.4  790  pm4.44  791  pm4.78i  794  pm4.45  796  pm3.48  797  pm2.76  820  orabs  826  ordi  828  andi  830  pm4.72  839  biort  841  dcim  853  pm2.54dc  903  pm2.85dc  917  dcor  948  pm5.71dc  974  dedlema  982  3mix1  1197  xoranor  1426  19.33  1537  hbor  1599  nford  1620  19.30dc  1680  19.43  1681  19.32r  1732  moor  2158  r19.32r  2697  ssun1  3392  undif3ss  3492  reuun1  3515  prmg  3835  opthpr  3897  exmidn0m  4340  issod  4466  elelsuc  4556  ordtri2or2exmidlem  4675  regexmidlem1  4682  fununmo  5426  nndceq  6776  nndcel  6777  swoord1  6840  swoord2  6841  exmidontri2or  7609  addlocprlem  7909  msqge0  8953  mulge0  8956  ltleap  8969  nn1m1nn  9332  elnnz  9666  zletric  9700  zlelttric  9701  zmulcl  9710  zdceq  9732  zdcle  9733  zdclt  9734  ltpnf  10200  xrlttri3  10217  xrpnfdc  10262  xrmnfdc  10263  fzdcel  10462  qletric  10694  qlelttric  10695  qdceq  10697  qdclt  10698  qsqeqor  11109  hashfiv01gt1  11244  isum  12178  iprodap  12373  iprodap0  12375  nn0o1gt2  12698  prm23lt5  13072  4sqlem17  13216  gsummptfidmsplit  14255  ppiprm  16271  ppidif  16281  gausslemma2dlem0f  16390  bj-trdc  16997  bj-nn0suc0  17193  triap  17296  tridceq  17325