Theorem olc 668

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

Syntax hints:   → wi 4   ∧ wa 103   ∨ wo 665

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm1.4  682  olci  687  pm2.07  692  pm2.46  694  biorf  699  pm1.5  718  pm2.41  729  pm3.48  735  ordi  766  andi  768  pm4.72  773  pm2.54dc  829  oibabs  839  pm4.78i  847  pm2.85dc  850  dcor  882  dedlemb  917  xoranor  1314  19.33  1419  hbor  1484  nford  1505  19.30dc  1564  19.43  1565  19.32r  1616  euor2  2007  mooran2  2022  r19.32r  2515  undif3ss  3261  undif4  3349  issod  4155  onsucelsucexmid  4359  sucprcreg  4378  0elnn  4445  acexmidlemph  5659  nntri3or  6268  swoord1  6335  swoord2  6336  addlocprlem  7148  nqprloc  7158  apreap  8118  zletric  8848  zlelttric  8849  zmulcl  8857  zdceq  8876  zdcle  8877  zdclt  8878  nn0lt2  8882  elnn1uz2  9148  mnflt  9307  mnfltpnf  9309  xrltso  9320  fzdcel  9508  fzm1  9568  qletric  9709  qlelttric  9710  qdceq  9712  nn0o1gt2  11237  decidin  11963