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  7564  exmidontri2or  7602  addlocprlem  7902  nqprloc  7912  apreap  8915  zletric  9688  zlelttric  9689  zmulcl  9698  zdceq  9720  zdcle  9721  zdclt  9722  nn0lt2  9727  elnn1uz2  10007  mnflt  10185  mnfltpnf  10187  xrltso  10198  fzdcel  10444  fzm1  10507  qletric  10676  qlelttric  10677  qdceq  10679  qdclt  10680  qsqeqor  11087  zzlesq  11146  nn0o1gt2  12672  prm23lt5  13042  gausslemma2dlem0f  16173  umgrupgr  16353  umgrislfupgrenlem  16371  usgruspgr  16424  konigsbergssiedgwen  16727  bj-fadc  16782  decidin  16825  triap  17078  tridceq  17106