Theorem olc 664

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

Syntax hints:   → wi 4   ∧ wa 102   ∨ wo 661

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm1.4  678  olci  683  pm2.07  688  pm2.46  690  biorf  695  pm1.5  714  pm2.41  725  pm3.48  731  ordi  762  andi  764  pm4.72  769  pm2.54dc  823  oibabs  833  pm4.78i  841  pm2.85dc  844  dcor  876  dedlemb  911  xoranor  1308  19.33  1413  hbor  1478  nford  1499  19.30dc  1558  19.43  1559  19.32r  1610  euor2  1999  mooran2  2014  r19.32r  2501  undif3ss  3225  undif4  3306  issod  4074  onsucelsucexmid  4273  sucprcreg  4292  0elnn  4358  acexmidlemph  5525  nntri3or  6095  swoord1  6158  swoord2  6159  addlocprlem  6725  nqprloc  6735  apreap  7687  zletric  8395  zlelttric  8396  zmulcl  8404  zdceq  8423  zdcle  8424  zdclt  8425  nn0lt2  8429  elnn1uz2  8694  mnflt  8858  mnfltpnf  8860  xrltso  8871  fzdcel  9059  fzm1  9117  qletric  9253  qlelttric  9254  qdceq  9256  nn0o1gt2  10305