Theorem olc 723

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  oibabs  726  pm1.4  739  olci  744  pm2.07  749  pm2.46  751  biorf  756  pm1.5  777  pm2.41  788  pm4.78i  794  pm3.48  797  ordi  828  andi  830  pm4.72  839  stdcn  859  pm2.54dc  903  pm2.85dc  917  dcor  948  dedlemb  983  anifpdc  999  xoranor  1426  19.33  1537  hbor  1599  nford  1620  19.30dc  1680  19.43  1681  19.32r  1732  euor2  2145  mooran2  2160  r19.32r  2697  undif3ss  3492  undif4  3586  issod  4459  onsucelsucexmid  4672  sucprcreg  4691  0elnn  4761  acexmidlemph  6068  nntri3or  6756  swoord1  6826  swoord2  6827  exmidaclem  7554  exmidontri2or  7592  addlocprlem  7892  nqprloc  7902  apreap  8905  zletric  9667  zlelttric  9668  zmulcl  9677  zdceq  9699  zdcle  9700  zdclt  9701  nn0lt2  9706  elnn1uz2  9986  mnflt  10164  mnfltpnf  10166  xrltso  10177  fzdcel  10423  fzm1  10485  qletric  10654  qlelttric  10655  qdceq  10657  qdclt  10658  qsqeqor  11065  zzlesq  11124  nn0o1gt2  12650  prm23lt5  13020  gausslemma2dlem0f  16087  umgrupgr  16267  umgrislfupgrenlem  16285  usgruspgr  16338  konigsbergssiedgwen  16641  bj-fadc  16696  decidin  16739  triap  16983  tridceq  17011