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  6517  nqprloc  6527  apreap  7351  zletric  8045  zlelttric  8046  zmulcl  8053  zdceq  8072  zdcle  8073  zdclt  8074  nn0lt2  8078  elnn1uz2  8300  mnflt  8454  mnfltpnf  8456  xrltso  8467  fzdcel  8654  fzm1  8712