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  6010  nntri3or  6660  swoord1  6730  swoord2  6731  exmidaclem  7422  exmidontri2or  7460  addlocprlem  7754  nqprloc  7764  apreap  8766  zletric  9522  zlelttric  9523  zmulcl  9532  zdceq  9554  zdcle  9555  zdclt  9556  nn0lt2  9560  elnn1uz2  9840  mnflt  10017  mnfltpnf  10019  xrltso  10030  fzdcel  10274  fzm1  10334  qletric  10500  qlelttric  10501  qdceq  10503  qdclt  10504  qsqeqor  10911  zzlesq  10969  nn0o1gt2  12465  prm23lt5  12835  gausslemma2dlem0f  15782  umgrupgr  15962  umgrislfupgrenlem  15980  usgruspgr  16033  bj-fadc  16350  decidin  16393  triap  16633  tridceq  16660