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  1495  hbor  1557  nford  1578  19.30dc  1638  19.43  1639  19.32r  1691  euor2  2100  mooran2  2115  r19.32r  2640  undif3ss  3420  undif4  3509  issod  4350  onsucelsucexmid  4562  sucprcreg  4581  0elnn  4651  acexmidlemph  5911  nntri3or  6546  swoord1  6616  swoord2  6617  exmidaclem  7268  exmidontri2or  7303  addlocprlem  7595  nqprloc  7605  apreap  8606  zletric  9361  zlelttric  9362  zmulcl  9370  zdceq  9392  zdcle  9393  zdclt  9394  nn0lt2  9398  elnn1uz2  9672  mnflt  9849  mnfltpnf  9851  xrltso  9862  fzdcel  10106  fzm1  10166  qletric  10311  qlelttric  10312  qdceq  10314  qdclt  10315  qsqeqor  10721  zzlesq  10779  nn0o1gt2  12046  prm23lt5  12401  gausslemma2dlem0f  15170  bj-fadc  15246  decidin  15289  triap  15519  tridceq  15546