Theorem olc 712

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 711	. . 3 ⊢ (((𝜓 ∨ 𝜑) → (𝜓 ∨ 𝜑)) ↔ ((𝜓 → (𝜓 ∨ 𝜑)) ∧ (𝜑 → (𝜓 ∨ 𝜑))))
3	1, 2	mpbi 145	. 2 ⊢ ((𝜓 → (𝜓 ∨ 𝜑)) ∧ (𝜑 → (𝜓 ∨ 𝜑)))
4	3	simpri 113	1 ⊢ (𝜑 → (𝜓 ∨ 𝜑))

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-io 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  oibabs  715  pm1.4  728  olci  733  pm2.07  738  pm2.46  740  biorf  745  pm1.5  766  pm2.41  777  pm4.78i  783  pm3.48  786  ordi  817  andi  819  pm4.72  828  stdcn  848  pm2.54dc  892  pm2.85dc  906  dcor  937  dedlemb  972  xoranor  1388  19.33  1498  hbor  1560  nford  1581  19.30dc  1641  19.43  1642  19.32r  1694  euor2  2103  mooran2  2118  r19.32r  2643  undif3ss  3425  undif4  3514  issod  4355  onsucelsucexmid  4567  sucprcreg  4586  0elnn  4656  acexmidlemph  5918  nntri3or  6560  swoord1  6630  swoord2  6631  exmidaclem  7291  exmidontri2or  7326  addlocprlem  7619  nqprloc  7629  apreap  8631  zletric  9387  zlelttric  9388  zmulcl  9396  zdceq  9418  zdcle  9419  zdclt  9420  nn0lt2  9424  elnn1uz2  9698  mnflt  9875  mnfltpnf  9877  xrltso  9888  fzdcel  10132  fzm1  10192  qletric  10348  qlelttric  10349  qdceq  10351  qdclt  10352  qsqeqor  10759  zzlesq  10817  nn0o1gt2  12087  prm23lt5  12457  gausslemma2dlem0f  15379  bj-fadc  15484  decidin  15527  triap  15760  tridceq  15787