Theorem olc 719

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  oibabs  722  pm1.4  735  olci  740  pm2.07  745  pm2.46  747  biorf  752  pm1.5  773  pm2.41  784  pm4.78i  790  pm3.48  793  ordi  824  andi  826  pm4.72  835  stdcn  855  pm2.54dc  899  pm2.85dc  913  dcor  944  dedlemb  979  anifpdc  995  xoranor  1422  19.33  1533  hbor  1595  nford  1616  19.30dc  1676  19.43  1677  19.32r  1728  euor2  2138  mooran2  2153  r19.32r  2680  undif3ss  3470  undif4  3559  issod  4422  onsucelsucexmid  4634  sucprcreg  4653  0elnn  4723  acexmidlemph  6021  nntri3or  6704  swoord1  6774  swoord2  6775  exmidaclem  7483  exmidontri2or  7521  addlocprlem  7815  nqprloc  7825  apreap  8826  zletric  9584  zlelttric  9585  zmulcl  9594  zdceq  9616  zdcle  9617  zdclt  9618  nn0lt2  9622  elnn1uz2  9902  mnflt  10079  mnfltpnf  10081  xrltso  10092  fzdcel  10337  fzm1  10397  qletric  10564  qlelttric  10565  qdceq  10567  qdclt  10568  qsqeqor  10975  zzlesq  11033  nn0o1gt2  12546  prm23lt5  12916  gausslemma2dlem0f  15873  umgrupgr  16053  umgrislfupgrenlem  16071  usgruspgr  16124  konigsbergssiedgwen  16427  bj-fadc  16472  decidin  16515  triap  16761  tridceq  16789