Theorem olc 632

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

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

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

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm1.4  646  olci  651  pm2.07  656  pm2.46  658  biorf  663  pm1.5  682  pm2.41  693  pm3.48  699  ordi  729  andi  731  pm4.72  736  pm2.54dc  790  oibabs  800  pm4.78i  808  pm2.85dc  811  dcor  843  dedlemb  877  xoranor  1268  19.33  1373  hbor  1438  nford  1459  19.30dc  1518  19.43  1519  19.32r  1570  euor2  1958  mooran2  1973  r19.32r  2457  undif3ss  3198  undif4  3284  issod  4056  onsucelsucexmid  4255  sucprcreg  4273  0elnn  4340  acexmidlemph  5505  nntri3or  6072  swoord1  6135  swoord2  6136  addlocprlem  6633  nqprloc  6643  apreap  7578  zletric  8289  zlelttric  8290  zmulcl  8297  zdceq  8316  zdcle  8317  zdclt  8318  nn0lt2  8322  elnn1uz2  8544  mnflt  8704  mnfltpnf  8706  xrltso  8717  fzdcel  8904  fzm1  8962  qletric  9099  qlelttric  9100  qdceq  9102