Theorem olc 713

Description: Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.)

Assertion

Ref	Expression
olc	⊢ (𝜑 → (𝜓 ∨ 𝜑))

Proof of Theorem olc

Step	Hyp	Ref	Expression
1		id 19	. . 3 ⊢ ((𝜓 ∨ 𝜑) → (𝜓 ∨ 𝜑))
2		jaob 712	. . 3 ⊢ (((𝜓 ∨ 𝜑) → (𝜓 ∨ 𝜑)) ↔ ((𝜓 → (𝜓 ∨ 𝜑)) ∧ (𝜑 → (𝜓 ∨ 𝜑))))
3	1, 2	mpbi 145	. 2 ⊢ ((𝜓 → (𝜓 ∨ 𝜑)) ∧ (𝜑 → (𝜓 ∨ 𝜑)))
4	3	simpri 113	1 ⊢ (𝜑 → (𝜓 ∨ 𝜑))

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  oibabs  716  pm1.4  729  olci  734  pm2.07  739  pm2.46  741  biorf  746  pm1.5  767  pm2.41  778  pm4.78i  784  pm3.48  787  ordi  818  andi  820  pm4.72  829  stdcn  849  pm2.54dc  893  pm2.85dc  907  dcor  938  dedlemb  973  xoranor  1397  19.33  1508  hbor  1570  nford  1591  19.30dc  1651  19.43  1652  19.32r  1704  euor2  2114  mooran2  2129  r19.32r  2654  undif3ss  3442  undif4  3531  issod  4384  onsucelsucexmid  4596  sucprcreg  4615  0elnn  4685  acexmidlemph  5960  nntri3or  6602  swoord1  6672  swoord2  6673  exmidaclem  7351  exmidontri2or  7389  addlocprlem  7683  nqprloc  7693  apreap  8695  zletric  9451  zlelttric  9452  zmulcl  9461  zdceq  9483  zdcle  9484  zdclt  9485  nn0lt2  9489  elnn1uz2  9763  mnflt  9940  mnfltpnf  9942  xrltso  9953  fzdcel  10197  fzm1  10257  qletric  10421  qlelttric  10422  qdceq  10424  qdclt  10425  qsqeqor  10832  zzlesq  10890  nn0o1gt2  12331  prm23lt5  12701  gausslemma2dlem0f  15646  umgrupgr  15823  umgrislfupgrenlem  15836  bj-fadc  15890  decidin  15933  triap  16170  tridceq  16197