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  3486  undif4  3575  issod  4445  onsucelsucexmid  4657  sucprcreg  4676  0elnn  4746  acexmidlemph  6051  nntri3or  6739  swoord1  6809  swoord2  6810  exmidaclem  7528  exmidontri2or  7566  addlocprlem  7866  nqprloc  7876  apreap  8878  zletric  9638  zlelttric  9639  zmulcl  9648  zdceq  9670  zdcle  9671  zdclt  9672  nn0lt2  9677  elnn1uz2  9957  mnflt  10135  mnfltpnf  10137  xrltso  10148  fzdcel  10394  fzm1  10456  qletric  10625  qlelttric  10626  qdceq  10628  qdclt  10629  qsqeqor  11036  zzlesq  11095  nn0o1gt2  12616  prm23lt5  12986  gausslemma2dlem0f  16053  umgrupgr  16233  umgrislfupgrenlem  16251  usgruspgr  16304  konigsbergssiedgwen  16607  bj-fadc  16652  decidin  16695  triap  16939  tridceq  16967