Theorem orc 719

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.67-2  720  pm1.4  734  orci  738  orcd  740  orcs  742  pm2.45  745  biorfi  753  pm1.5  772  pm2.4  785  pm4.44  786  pm4.78i  789  pm4.45  791  pm3.48  792  pm2.76  815  orabs  821  ordi  823  andi  825  pm4.72  834  biort  836  dcim  848  pm2.54dc  898  pm2.85dc  912  dcor  943  pm5.71dc  969  dedlema  977  3mix1  1192  xoranor  1421  19.33  1532  hbor  1594  nford  1615  19.30dc  1675  19.43  1676  19.32r  1728  moor  2151  r19.32r  2679  ssun1  3370  undif3ss  3468  reuun1  3489  prmg  3794  opthpr  3855  exmidn0m  4291  issod  4416  elelsuc  4506  ordtri2or2exmidlem  4624  regexmidlem1  4631  fununmo  5372  nndceq  6667  nndcel  6668  swoord1  6731  swoord2  6732  exmidontri2or  7461  addlocprlem  7755  msqge0  8796  mulge0  8799  ltleap  8812  nn1m1nn  9161  elnnz  9489  zletric  9523  zlelttric  9524  zmulcl  9533  zdceq  9555  zdcle  9556  zdclt  9557  ltpnf  10015  xrlttri3  10032  xrpnfdc  10077  xrmnfdc  10078  fzdcel  10275  qletric  10502  qlelttric  10503  qdceq  10505  qdclt  10506  qsqeqor  10913  hashfiv01gt1  11045  isum  11951  iprodap  12146  iprodap0  12148  nn0o1gt2  12471  prm23lt5  12841  4sqlem17  12985  gausslemma2dlem0f  15789  bj-trdc  16374  bj-nn0suc0  16571  triap  16659  tridceq  16686