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  8917  zletric  9692  zlelttric  9693  zmulcl  9702  zdceq  9724  zdcle  9725  zdclt  9726  nn0lt2  9731  elnn1uz2  10016  mnflt  10195  mnfltpnf  10197  xrltso  10208  fzdcel  10454  fzm1  10517  qletric  10686  qlelttric  10687  qdceq  10689  qdclt  10690  qsqeqor  11100  zzlesq  11159  nn0o1gt2  12688  prm23lt5  13062  gausslemma2dlem0f  16271  umgrupgr  16451  umgrislfupgrenlem  16469  usgruspgr  16522  konigsbergssiedgwen  16825  bj-fadc  16880  decidin  16923  triap  17176  tridceq  17204