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  2141  mooran2  2156  r19.32r  2691  undif3ss  3484  undif4  3573  issod  4442  onsucelsucexmid  4654  sucprcreg  4673  0elnn  4743  acexmidlemph  6045  nntri3or  6728  swoord1  6798  swoord2  6799  exmidaclem  7517  exmidontri2or  7555  addlocprlem  7852  nqprloc  7862  apreap  8863  zletric  9623  zlelttric  9624  zmulcl  9633  zdceq  9655  zdcle  9656  zdclt  9657  nn0lt2  9662  elnn1uz2  9942  mnflt  10119  mnfltpnf  10121  xrltso  10132  fzdcel  10377  fzm1  10438  qletric  10605  qlelttric  10606  qdceq  10608  qdclt  10609  qsqeqor  11016  zzlesq  11074  nn0o1gt2  12595  prm23lt5  12965  gausslemma2dlem0f  15944  umgrupgr  16124  umgrislfupgrenlem  16142  usgruspgr  16195  konigsbergssiedgwen  16498  bj-fadc  16543  decidin  16586  triap  16830  tridceq  16858