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  1356  19.33  1461  hbor  1526  nford  1547  19.30dc  1607  19.43  1608  19.32r  1659  euor2  2058  mooran2  2073  r19.32r  2581  undif3ss  3342  undif4  3430  issod  4249  onsucelsucexmid  4453  sucprcreg  4472  0elnn  4540  acexmidlemph  5775  nntri3or  6397  swoord1  6466  swoord2  6467  exmidaclem  7081  addlocprlem  7367  nqprloc  7377  apreap  8373  zletric  9122  zlelttric  9123  zmulcl  9131  zdceq  9150  zdcle  9151  zdclt  9152  nn0lt2  9156  elnn1uz2  9428  mnflt  9599  mnfltpnf  9601  xrltso  9612  fzdcel  9851  fzm1  9911  qletric  10052  qlelttric  10053  qdceq  10055  nn0o1gt2  11638  bj-fadc  13131  decidin  13175  triap  13399