Theorem orc 632

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

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

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

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm2.67-2  633  pm1.4  645  orci  649  orcd  651  orcs  653  pm2.45  656  biorfi  664  pm1.5  681  pm2.4  694  pm4.44  695  pm4.45  697  pm3.48  698  pm2.76  720  orabs  726  ordi  728  andi  730  pm4.72  735  biort  737  dcim  783  pm2.54dc  789  pm4.78i  807  pm2.85dc  810  dcor  842  pm5.71dc  867  dedlema  875  3mix1  1072  xoranor  1267  19.33  1370  hbor  1435  nford  1456  19.30dc  1515  19.43  1516  19.32r  1567  moor  1968  r19.32r  2451  ssun1  3100  undif3ss  3192  reuun1  3213  prmg  3480  opthpr  3534  issod  4047  elelsuc  4112  regexmidlem1  4218  nndceq  6015  nndcel  6016  swoord1  6071  swoord2  6072  addlocprlem  6518  msqge0  7400  mulge0  7403  ltleap  7413  nn1m1nn  7713  elnnz  8031  zletric  8065  zlelttric  8066  zmulcl  8073  zdceq  8092  zdcle  8093  zdclt  8094  ltpnf  8472  xrlttri3  8488  fzdcel  8674  bj-nn0suc0  9410