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  4410  onsucelsucexmid  4622  sucprcreg  4641  0elnn  4711  acexmidlemph  6000  nntri3or  6647  swoord1  6717  swoord2  6718  exmidaclem  7401  exmidontri2or  7439  addlocprlem  7733  nqprloc  7743  apreap  8745  zletric  9501  zlelttric  9502  zmulcl  9511  zdceq  9533  zdcle  9534  zdclt  9535  nn0lt2  9539  elnn1uz2  9814  mnflt  9991  mnfltpnf  9993  xrltso  10004  fzdcel  10248  fzm1  10308  qletric  10473  qlelttric  10474  qdceq  10476  qdclt  10477  qsqeqor  10884  zzlesq  10942  nn0o1gt2  12432  prm23lt5  12802  gausslemma2dlem0f  15749  umgrupgr  15928  umgrislfupgrenlem  15944  usgruspgr  15997  bj-fadc  16201  decidin  16244  triap  16485  tridceq  16512