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  4466  onsucelsucexmid  4679  sucprcreg  4698  0elnn  4768  acexmidlemph  6081  nntri3or  6770  swoord1  6840  swoord2  6841  exmidaclem  7570  exmidontri2or  7608  addlocprlem  7908  nqprloc  7918  apreap  8923  zletric  9699  zlelttric  9700  zmulcl  9709  zdceq  9731  zdcle  9732  zdclt  9733  nn0lt2  9738  elnn1uz2  10023  mnflt  10202  mnfltpnf  10204  xrltso  10215  fzdcel  10461  fzm1  10524  qletric  10693  qlelttric  10694  qdceq  10696  qdclt  10697  qsqeqor  11108  zzlesq  11167  nn0o1gt2  12697  prm23lt5  13071  gausslemma2dlem0f  16378  umgrupgr  16558  umgrislfupgrenlem  16576  usgruspgr  16629  konigsbergssiedgwen  16932  bj-fadc  16987  decidin  17030  triap  17284  tridceq  17313