Theorem olc 718

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  oibabs  721  pm1.4  734  olci  739  pm2.07  744  pm2.46  746  biorf  751  pm1.5  772  pm2.41  783  pm4.78i  789  pm3.48  792  ordi  823  andi  825  pm4.72  834  stdcn  854  pm2.54dc  898  pm2.85dc  912  dcor  943  dedlemb  978  anifpdc  994  xoranor  1421  19.33  1532  hbor  1594  nford  1615  19.30dc  1675  19.43  1676  19.32r  1728  euor2  2138  mooran2  2153  r19.32r  2679  undif3ss  3468  undif4  3557  issod  4416  onsucelsucexmid  4628  sucprcreg  4647  0elnn  4717  acexmidlemph  6011  nntri3or  6661  swoord1  6731  swoord2  6732  exmidaclem  7423  exmidontri2or  7461  addlocprlem  7755  nqprloc  7765  apreap  8767  zletric  9523  zlelttric  9524  zmulcl  9533  zdceq  9555  zdcle  9556  zdclt  9557  nn0lt2  9561  elnn1uz2  9841  mnflt  10018  mnfltpnf  10020  xrltso  10031  fzdcel  10275  fzm1  10335  qletric  10502  qlelttric  10503  qdceq  10505  qdclt  10506  qsqeqor  10913  zzlesq  10971  nn0o1gt2  12484  prm23lt5  12854  gausslemma2dlem0f  15802  umgrupgr  15982  umgrislfupgrenlem  16000  usgruspgr  16053  konigsbergssiedgwen  16356  bj-fadc  16401  decidin  16444  triap  16684  tridceq  16712