Theorem olc 723

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 722	. . 3 ⊢ (((𝜓 ∨ 𝜑) → (𝜓 ∨ 𝜑)) ↔ ((𝜓 → (𝜓 ∨ 𝜑)) ∧ (𝜑 → (𝜓 ∨ 𝜑))))
3	1, 2	mpbi 145	. 2 ⊢ ((𝜓 → (𝜓 ∨ 𝜑)) ∧ (𝜑 → (𝜓 ∨ 𝜑)))
4	3	simpri 113	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-ia2 107  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  oibabs  726  pm1.4  739  olci  744  pm2.07  749  pm2.46  751  biorf  756  pm1.5  777  pm2.41  788  pm4.78i  794  pm3.48  797  ordi  828  andi  830  pm4.72  839  stdcn  859  pm2.54dc  903  pm2.85dc  917  dcor  948  dedlemb  983  anifpdc  999  xoranor  1426  19.33  1537  hbor  1599  nford  1620  19.30dc  1680  19.43  1681  19.32r  1732  euor2  2145  mooran2  2160  r19.32r  2697  undif3ss  3492  undif4  3587  issod  4464  onsucelsucexmid  4677  sucprcreg  4696  0elnn  4766  acexmidlemph  6078  nntri3or  6766  swoord1  6836  swoord2  6837  exmidaclem  7565  exmidontri2or  7603  addlocprlem  7903  nqprloc  7913  apreap  8918  zletric  9693  zlelttric  9694  zmulcl  9703  zdceq  9725  zdcle  9726  zdclt  9727  nn0lt2  9732  elnn1uz2  10017  mnflt  10196  mnfltpnf  10198  xrltso  10209  fzdcel  10455  fzm1  10518  qletric  10687  qlelttric  10688  qdceq  10690  qdclt  10691  qsqeqor  11102  zzlesq  11161  nn0o1gt2  12691  prm23lt5  13065  gausslemma2dlem0f  16339  umgrupgr  16519  umgrislfupgrenlem  16537  usgruspgr  16590  konigsbergssiedgwen  16893  bj-fadc  16948  decidin  16991  triap  17244  tridceq  17273