Theorem olc 701

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

Syntax hints:   → wi 4   ∧ wa 103   ∨ wo 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  oibabs  704  pm1.4  717  olci  722  pm2.07  727  pm2.46  729  biorf  734  pm1.5  755  pm2.41  766  pm4.78i  772  pm3.48  775  ordi  806  andi  808  pm4.72  817  stdcn  837  pm2.54dc  881  pm2.85dc  895  dcor  925  dedlemb  960  xoranor  1367  19.33  1472  hbor  1534  nford  1555  19.30dc  1615  19.43  1616  19.32r  1668  euor2  2072  mooran2  2087  r19.32r  2611  undif3ss  3382  undif4  3470  issod  4296  onsucelsucexmid  4506  sucprcreg  4525  0elnn  4595  acexmidlemph  5834  nntri3or  6457  swoord1  6526  swoord2  6527  exmidaclem  7160  exmidontri2or  7195  addlocprlem  7472  nqprloc  7482  apreap  8481  zletric  9231  zlelttric  9232  zmulcl  9240  zdceq  9262  zdcle  9263  zdclt  9264  nn0lt2  9268  elnn1uz2  9541  mnflt  9715  mnfltpnf  9717  xrltso  9728  fzdcel  9971  fzm1  10031  qletric  10175  qlelttric  10176  qdceq  10178  qsqeqor  10561  nn0o1gt2  11838  prm23lt5  12191  bj-fadc  13595  decidin  13638  triap  13868  tridceq  13895