Theorem olc 631

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

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

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

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm1.4  645  olci  650  pm2.07  655  pm2.46  657  biorf  662  pm1.5  681  pm2.41  692  pm3.48  698  ordi  728  andi  730  pm4.72  735  pm2.54dc  789  oibabs  799  pm4.78i  807  pm2.85dc  810  dcor  842  dedlemb  876  xoranor  1267  19.33  1370  hbor  1435  nford  1456  19.30dc  1515  19.43  1516  19.32r  1567  euor2  1955  mooran2  1970  r19.32r  2451  undif3ss  3192  undif4  3278  issod  4047  onsucelsucexmid  4215  sucprcreg  4227  0elnn  4283  acexmidlemph  5448  nntri3or  6011  swoord1  6071  swoord2  6072  addlocprlem  6518  nqprloc  6528  apreap  7371  zletric  8065  zlelttric  8066  zmulcl  8073  zdceq  8092  zdcle  8093  zdclt  8094  nn0lt2  8098  elnn1uz2  8320  mnflt  8474  mnfltpnf  8476  xrltso  8487  fzdcel  8674  fzm1  8732