Theorem olc 712

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

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 709

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  oibabs  715  pm1.4  728  olci  733  pm2.07  738  pm2.46  740  biorf  745  pm1.5  766  pm2.41  777  pm4.78i  783  pm3.48  786  ordi  817  andi  819  pm4.72  828  stdcn  848  pm2.54dc  892  pm2.85dc  906  dcor  937  dedlemb  972  xoranor  1388  19.33  1495  hbor  1557  nford  1578  19.30dc  1638  19.43  1639  19.32r  1691  euor2  2100  mooran2  2115  r19.32r  2640  undif3ss  3421  undif4  3510  issod  4351  onsucelsucexmid  4563  sucprcreg  4582  0elnn  4652  acexmidlemph  5912  nntri3or  6548  swoord1  6618  swoord2  6619  exmidaclem  7270  exmidontri2or  7305  addlocprlem  7597  nqprloc  7607  apreap  8608  zletric  9364  zlelttric  9365  zmulcl  9373  zdceq  9395  zdcle  9396  zdclt  9397  nn0lt2  9401  elnn1uz2  9675  mnflt  9852  mnfltpnf  9854  xrltso  9865  fzdcel  10109  fzm1  10169  qletric  10314  qlelttric  10315  qdceq  10317  qdclt  10318  qsqeqor  10724  zzlesq  10782  nn0o1gt2  12049  prm23lt5  12404  gausslemma2dlem0f  15211  bj-fadc  15316  decidin  15359  triap  15589  tridceq  15616