Theorem olc 711

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

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 708

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  oibabs  714  pm1.4  727  olci  732  pm2.07  737  pm2.46  739  biorf  744  pm1.5  765  pm2.41  776  pm4.78i  782  pm3.48  785  ordi  816  andi  818  pm4.72  827  stdcn  847  pm2.54dc  891  pm2.85dc  905  dcor  935  dedlemb  970  xoranor  1377  19.33  1484  hbor  1546  nford  1567  19.30dc  1627  19.43  1628  19.32r  1680  euor2  2084  mooran2  2099  r19.32r  2623  undif3ss  3398  undif4  3487  issod  4321  onsucelsucexmid  4531  sucprcreg  4550  0elnn  4620  acexmidlemph  5871  nntri3or  6497  swoord1  6567  swoord2  6568  exmidaclem  7210  exmidontri2or  7245  addlocprlem  7537  nqprloc  7547  apreap  8547  zletric  9300  zlelttric  9301  zmulcl  9309  zdceq  9331  zdcle  9332  zdclt  9333  nn0lt2  9337  elnn1uz2  9610  mnflt  9786  mnfltpnf  9788  xrltso  9799  fzdcel  10043  fzm1  10103  qletric  10247  qlelttric  10248  qdceq  10250  qsqeqor  10634  nn0o1gt2  11913  prm23lt5  12266  bj-fadc  14694  decidin  14737  triap  14966  tridceq  14993