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  4367  onsucelsucexmid  4579  sucprcreg  4598  0elnn  4668  acexmidlemph  5939  nntri3or  6581  swoord1  6651  swoord2  6652  exmidaclem  7322  exmidontri2or  7357  addlocprlem  7650  nqprloc  7660  apreap  8662  zletric  9418  zlelttric  9419  zmulcl  9428  zdceq  9450  zdcle  9451  zdclt  9452  nn0lt2  9456  elnn1uz2  9730  mnflt  9907  mnfltpnf  9909  xrltso  9920  fzdcel  10164  fzm1  10224  qletric  10386  qlelttric  10387  qdceq  10389  qdclt  10390  qsqeqor  10797  zzlesq  10855  nn0o1gt2  12249  prm23lt5  12619  gausslemma2dlem0f  15564  bj-fadc  15727  decidin  15770  triap  16005  tridceq  16032