Theorem olc 700

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  oibabs  703  pm1.4  716  olci  721  pm2.07  726  pm2.46  728  biorf  733  pm1.5  754  pm2.41  765  pm4.78i  771  pm3.48  774  ordi  805  andi  807  pm4.72  812  stdcn  832  pm2.54dc  876  pm2.85dc  890  dcor  919  dedlemb  954  xoranor  1355  19.33  1460  hbor  1525  nford  1546  19.30dc  1606  19.43  1607  19.32r  1658  euor2  2057  mooran2  2072  r19.32r  2578  undif3ss  3337  undif4  3425  issod  4241  onsucelsucexmid  4445  sucprcreg  4464  0elnn  4532  acexmidlemph  5767  nntri3or  6389  swoord1  6458  swoord2  6459  exmidaclem  7064  addlocprlem  7343  nqprloc  7353  apreap  8349  zletric  9098  zlelttric  9099  zmulcl  9107  zdceq  9126  zdcle  9127  zdclt  9128  nn0lt2  9132  elnn1uz2  9401  mnflt  9569  mnfltpnf  9571  xrltso  9582  fzdcel  9820  fzm1  9880  qletric  10021  qlelttric  10022  qdceq  10024  nn0o1gt2  11602  bj-fadc  12960  decidin  13004  triap  13224