Theorem olc 713

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  oibabs  716  pm1.4  729  olci  734  pm2.07  739  pm2.46  741  biorf  746  pm1.5  767  pm2.41  778  pm4.78i  784  pm3.48  787  ordi  818  andi  820  pm4.72  829  stdcn  849  pm2.54dc  893  pm2.85dc  907  dcor  938  dedlemb  973  xoranor  1397  19.33  1507  hbor  1569  nford  1590  19.30dc  1650  19.43  1651  19.32r  1703  euor2  2112  mooran2  2127  r19.32r  2652  undif3ss  3434  undif4  3523  issod  4366  onsucelsucexmid  4578  sucprcreg  4597  0elnn  4667  acexmidlemph  5937  nntri3or  6579  swoord1  6649  swoord2  6650  exmidaclem  7320  exmidontri2or  7355  addlocprlem  7648  nqprloc  7658  apreap  8660  zletric  9416  zlelttric  9417  zmulcl  9426  zdceq  9448  zdcle  9449  zdclt  9450  nn0lt2  9454  elnn1uz2  9728  mnflt  9905  mnfltpnf  9907  xrltso  9918  fzdcel  10162  fzm1  10222  qletric  10384  qlelttric  10385  qdceq  10387  qdclt  10388  qsqeqor  10795  zzlesq  10853  nn0o1gt2  12216  prm23lt5  12586  gausslemma2dlem0f  15531  bj-fadc  15690  decidin  15733  triap  15968  tridceq  15995