Theorem orc 712

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.67-2  713  pm1.4  727  orci  731  orcd  733  orcs  735  pm2.45  738  biorfi  746  pm1.5  765  pm2.4  778  pm4.44  779  pm4.78i  782  pm4.45  784  pm3.48  785  pm2.76  808  orabs  814  ordi  816  andi  818  pm4.72  827  biort  829  dcim  841  pm2.54dc  891  pm2.85dc  905  dcor  935  pm5.71dc  961  dedlema  969  3mix1  1166  xoranor  1377  19.33  1484  hbor  1546  nford  1567  19.30dc  1627  19.43  1628  19.32r  1680  moor  2097  r19.32r  2623  ssun1  3300  undif3ss  3398  reuun1  3419  prmg  3715  opthpr  3774  exmidn0m  4203  issod  4321  elelsuc  4411  ordtri2or2exmidlem  4527  regexmidlem1  4534  nndceq  6503  nndcel  6504  swoord1  6567  swoord2  6568  exmidontri2or  7245  addlocprlem  7537  msqge0  8576  mulge0  8579  ltleap  8592  nn1m1nn  8940  elnnz  9266  zletric  9300  zlelttric  9301  zmulcl  9309  zdceq  9331  zdcle  9332  zdclt  9333  ltpnf  9783  xrlttri3  9800  xrpnfdc  9845  xrmnfdc  9846  fzdcel  10043  qletric  10247  qlelttric  10248  qdceq  10250  qsqeqor  10634  hashfiv01gt1  10765  isum  11396  iprodap  11591  iprodap0  11593  nn0o1gt2  11913  prm23lt5  12266  bj-trdc  14665  bj-nn0suc0  14863  triap  14939  tridceq  14966