Theorem olc 701

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  oibabs  704  pm1.4  717  olci  722  pm2.07  727  pm2.46  729  biorf  734  pm1.5  755  pm2.41  766  pm4.78i  772  pm3.48  775  ordi  806  andi  808  pm4.72  813  stdcn  833  pm2.54dc  877  pm2.85dc  891  dcor  920  dedlemb  955  xoranor  1359  19.33  1464  hbor  1526  nford  1547  19.30dc  1607  19.43  1608  19.32r  1660  euor2  2064  mooran2  2079  r19.32r  2603  undif3ss  3368  undif4  3456  issod  4279  onsucelsucexmid  4489  sucprcreg  4508  0elnn  4578  acexmidlemph  5817  nntri3or  6440  swoord1  6509  swoord2  6510  exmidaclem  7143  exmidontri2or  7178  addlocprlem  7455  nqprloc  7465  apreap  8462  zletric  9211  zlelttric  9212  zmulcl  9220  zdceq  9239  zdcle  9240  zdclt  9241  nn0lt2  9245  elnn1uz2  9518  mnflt  9690  mnfltpnf  9692  xrltso  9703  fzdcel  9942  fzm1  10002  qletric  10143  qlelttric  10144  qdceq  10146  nn0o1gt2  11796  bj-fadc  13337  decidin  13382  triap  13611  tridceq  13638