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  3396  undif4  3485  issod  4317  onsucelsucexmid  4527  sucprcreg  4546  0elnn  4616  acexmidlemph  5863  nntri3or  6489  swoord1  6559  swoord2  6560  exmidaclem  7202  exmidontri2or  7237  addlocprlem  7529  nqprloc  7539  apreap  8538  zletric  9291  zlelttric  9292  zmulcl  9300  zdceq  9322  zdcle  9323  zdclt  9324  nn0lt2  9328  elnn1uz2  9601  mnflt  9777  mnfltpnf  9779  xrltso  9790  fzdcel  10033  fzm1  10093  qletric  10237  qlelttric  10238  qdceq  10240  qsqeqor  10623  nn0o1gt2  11900  prm23lt5  12253  bj-fadc  14277  decidin  14320  triap  14548  tridceq  14575