Theorem olc 707

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  oibabs  710  pm1.4  723  olci  728  pm2.07  733  pm2.46  735  biorf  740  pm1.5  761  pm2.41  772  pm4.78i  778  pm3.48  781  ordi  812  andi  814  pm4.72  823  stdcn  843  pm2.54dc  887  pm2.85dc  901  dcor  931  dedlemb  966  xoranor  1373  19.33  1478  hbor  1540  nford  1561  19.30dc  1621  19.43  1622  19.32r  1674  euor2  2078  mooran2  2093  r19.32r  2617  undif3ss  3389  undif4  3478  issod  4305  onsucelsucexmid  4515  sucprcreg  4534  0elnn  4604  acexmidlemph  5850  nntri3or  6476  swoord1  6546  swoord2  6547  exmidaclem  7189  exmidontri2or  7224  addlocprlem  7501  nqprloc  7511  apreap  8510  zletric  9260  zlelttric  9261  zmulcl  9269  zdceq  9291  zdcle  9292  zdclt  9293  nn0lt2  9297  elnn1uz2  9570  mnflt  9744  mnfltpnf  9746  xrltso  9757  fzdcel  10000  fzm1  10060  qletric  10204  qlelttric  10205  qdceq  10207  qsqeqor  10590  nn0o1gt2  11868  prm23lt5  12221  bj-fadc  13874  decidin  13917  triap  14146  tridceq  14173