Theorem olc 619

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 618	. . 3 ⊢ (((ψ ∨ φ) → (ψ ∨ φ)) ↔ ((ψ → (ψ ∨ φ)) ∧ (φ → (ψ ∨ φ))))
3	1, 2	mpbi 133	. 2 ⊢ ((ψ → (ψ ∨ φ)) ∧ (φ → (ψ ∨ φ)))
4	3	simpri 106	1 ⊢ (φ → (ψ ∨ φ))

Syntax hints:   → wi 4   ∧ wa 97   ∨ wo 616

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-io 617

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm1.4  633  olci  638  pm2.07  643  pm2.46  645  biorf  650  pm1.5  669  pm2.41  680  pm3.48  686  ordi  717  andi  719  pm4.72  724  pm2.54dc  783  oibabs  793  pm4.78i  801  pm2.85dc  804  dcor  831  dedlemb  865  xoranor  1253  19.33  1353  hbor  1420  nford  1441  19.30dc  1500  19.43  1501  19.32r  1552  euor2  1940  mooran2  1955  r19.32r  2435  undif3ss  3175  undif4  3261  issod  4030  onsucelsucexmid  4199  sucprcreg  4211  0elnn  4267  acexmidlemph  5429  nntri3or  5987  swoord1  6046  swoord2  6047  addlocprlem  6390  nqprloc  6400