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  3424  undif4  3513  issod  4354  onsucelsucexmid  4566  sucprcreg  4585  0elnn  4655  acexmidlemph  5915  nntri3or  6551  swoord1  6621  swoord2  6622  exmidaclem  7275  exmidontri2or  7310  addlocprlem  7602  nqprloc  7612  apreap  8614  zletric  9370  zlelttric  9371  zmulcl  9379  zdceq  9401  zdcle  9402  zdclt  9403  nn0lt2  9407  elnn1uz2  9681  mnflt  9858  mnfltpnf  9860  xrltso  9871  fzdcel  10115  fzm1  10175  qletric  10331  qlelttric  10332  qdceq  10334  qdclt  10335  qsqeqor  10742  zzlesq  10800  nn0o1gt2  12070  prm23lt5  12432  gausslemma2dlem0f  15295  bj-fadc  15400  decidin  15443  triap  15673  tridceq  15700