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  3465  undif4  3554  issod  4411  onsucelsucexmid  4623  sucprcreg  4642  0elnn  4712  acexmidlemph  6003  nntri3or  6652  swoord1  6722  swoord2  6723  exmidaclem  7406  exmidontri2or  7444  addlocprlem  7738  nqprloc  7748  apreap  8750  zletric  9506  zlelttric  9507  zmulcl  9516  zdceq  9538  zdcle  9539  zdclt  9540  nn0lt2  9544  elnn1uz2  9819  mnflt  9996  mnfltpnf  9998  xrltso  10009  fzdcel  10253  fzm1  10313  qletric  10478  qlelttric  10479  qdceq  10481  qdclt  10482  qsqeqor  10889  zzlesq  10947  nn0o1gt2  12437  prm23lt5  12807  gausslemma2dlem0f  15754  umgrupgr  15933  umgrislfupgrenlem  15949  usgruspgr  16002  bj-fadc  16227  decidin  16270  triap  16511  tridceq  16538