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  1356  19.33  1461  hbor  1526  nford  1547  19.30dc  1607  19.43  1608  19.32r  1659  moor  2071  r19.32r  2581  ssun1  3244  undif3ss  3342  reuun1  3363  prmg  3652  opthpr  3707  exmidn0m  4132  issod  4249  elelsuc  4339  ordtri2or2exmidlem  4449  regexmidlem1  4456  nndceq  6403  nndcel  6404  swoord1  6466  swoord2  6467  addlocprlem  7367  msqge0  8402  mulge0  8405  ltleap  8418  nn1m1nn  8762  elnnz  9088  zletric  9122  zlelttric  9123  zmulcl  9131  zdceq  9150  zdcle  9151  zdclt  9152  ltpnf  9597  xrlttri3  9613  xrpnfdc  9655  xrmnfdc  9656  fzdcel  9851  qletric  10052  qlelttric  10053  qdceq  10055  hashfiv01gt1  10560  isum  11186  iprodap  11381  iprodap0  11383  nn0o1gt2  11638  bj-trdc  13130  bj-nn0suc0  13319  triap  13399