Theorem orc 620

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 618	. . 3 ⊢ (((φ ∨ ψ) → (φ ∨ ψ)) ↔ ((φ → (φ ∨ ψ)) ∧ (ψ → (φ ∨ ψ))))
3	1, 2	mpbi 133	. 2 ⊢ ((φ → (φ ∨ ψ)) ∧ (ψ → (φ ∨ ψ)))
4	3	simpli 104	1 ⊢ (φ → (φ ∨ ψ))

Syntax hints:   → wi 4   ∧ wa 97   ∨ wo 616

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

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm2.67-2  621  pm1.4  633  orci  637  orcd  639  orcs  641  pm2.45  644  biorfi  652  pm1.5  669  pm2.4  682  pm4.44  683  pm4.45  685  pm3.48  686  pm2.76  708  orabs  714  orabsOLD  715  ordi  717  andi  719  pm4.72  724  biort  726  dcim  772  pm2.54dc  778  pm4.78i  796  pm2.85dc  799  dcor  829  pm5.71dc  854  dedlema  862  3mix1  1059  xoranor  1251  19.33  1349  hbor  1416  nford  1437  19.30dc  1496  19.43  1497  19.32r  1548  moor  1949  r19.32r  2431  ssun1  3079  undif3ss  3171  reuun1  3192  prmg  3459  opthpr  3513  issod  4026  elelsuc  4091  regexmidlem1  4198  nndceq  5986  nndcel  5987  swoord1  6042  swoord2  6043  addlocprlem  6384  bj-nn0suc0  7368