Theorem olc 716

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  oibabs  719  pm1.4  732  olci  737  pm2.07  742  pm2.46  744  biorf  749  pm1.5  770  pm2.41  781  pm4.78i  787  pm3.48  790  ordi  821  andi  823  pm4.72  832  stdcn  852  pm2.54dc  896  pm2.85dc  910  dcor  941  dedlemb  976  anifpdc  992  xoranor  1419  19.33  1530  hbor  1592  nford  1613  19.30dc  1673  19.43  1674  19.32r  1726  euor2  2136  mooran2  2151  r19.32r  2677  undif3ss  3466  undif4  3555  issod  4414  onsucelsucexmid  4626  sucprcreg  4645  0elnn  4715  acexmidlemph  6006  nntri3or  6656  swoord1  6726  swoord2  6727  exmidaclem  7413  exmidontri2or  7451  addlocprlem  7745  nqprloc  7755  apreap  8757  zletric  9513  zlelttric  9514  zmulcl  9523  zdceq  9545  zdcle  9546  zdclt  9547  nn0lt2  9551  elnn1uz2  9831  mnflt  10008  mnfltpnf  10010  xrltso  10021  fzdcel  10265  fzm1  10325  qletric  10491  qlelttric  10492  qdceq  10494  qdclt  10495  qsqeqor  10902  zzlesq  10960  nn0o1gt2  12456  prm23lt5  12826  gausslemma2dlem0f  15773  umgrupgr  15953  umgrislfupgrenlem  15969  usgruspgr  16022  bj-fadc  16286  decidin  16329  triap  16569  tridceq  16596