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  6771  swoord1  6841  swoord2  6842  exmidaclem  7570  exmidontri2or  7608  addlocprlem  7908  nqprloc  7918  apreap  8923  zletric  9697  zlelttric  9698  zmulcl  9707  zdceq  9729  zdcle  9730  zdclt  9731  nn0lt2  9736  elnn1uz2  10022  mnflt  10201  mnfltpnf  10203  xrltso  10214  fzdcel  10460  fzm1  10523  qletric  10692  qlelttric  10693  qdceq  10695  qdclt  10696  qsqeqor  11107  zzlesq  11166  nn0o1gt2  12696  prm23lt5  13070  gausslemma2dlem0f  16395  umgrupgr  16575  umgrislfupgrenlem  16593  usgruspgr  16646  konigsbergssiedgwen  16949  bj-fadc  17004  decidin  17047  triap  17301  tridceq  17330