Theorem orc 702

Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.)

Assertion

Ref	Expression
orc	⊢ (𝜑 → (𝜑 ∨ 𝜓))

Proof of Theorem orc

Step	Hyp	Ref	Expression
1		id 19	. . 3 ⊢ ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜓))
2		jaob 700	. . 3 ⊢ (((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜓)) ↔ ((𝜑 → (𝜑 ∨ 𝜓)) ∧ (𝜓 → (𝜑 ∨ 𝜓))))
3	1, 2	mpbi 144	. 2 ⊢ ((𝜑 → (𝜑 ∨ 𝜓)) ∧ (𝜓 → (𝜑 ∨ 𝜓)))
4	3	simpli 110	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-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm2.67-2  703  pm1.4  717  orci  721  orcd  723  orcs  725  pm2.45  728  biorfi  736  pm1.5  755  pm2.4  768  pm4.44  769  pm4.78i  772  pm4.45  774  pm3.48  775  pm2.76  798  orabs  804  ordi  806  andi  808  pm4.72  813  biort  815  dcim  827  pm2.54dc  877  pm2.85dc  891  dcor  920  pm5.71dc  946  dedlema  954  3mix1  1151  xoranor  1359  19.33  1464  hbor  1526  nford  1547  19.30dc  1607  19.43  1608  19.32r  1660  moor  2077  r19.32r  2603  ssun1  3270  undif3ss  3368  reuun1  3389  prmg  3680  opthpr  3735  exmidn0m  4162  issod  4279  elelsuc  4369  ordtri2or2exmidlem  4485  regexmidlem1  4492  nndceq  6446  nndcel  6447  swoord1  6509  swoord2  6510  exmidontri2or  7178  addlocprlem  7455  msqge0  8491  mulge0  8494  ltleap  8507  nn1m1nn  8851  elnnz  9177  zletric  9211  zlelttric  9212  zmulcl  9220  zdceq  9239  zdcle  9240  zdclt  9241  ltpnf  9687  xrlttri3  9704  xrpnfdc  9746  xrmnfdc  9747  fzdcel  9942  qletric  10143  qlelttric  10144  qdceq  10146  hashfiv01gt1  10656  isum  11282  iprodap  11477  iprodap0  11479  nn0o1gt2  11796  bj-trdc  13335  bj-nn0suc0  13536  triap  13611  tridceq  13638