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  7360  mulge0  7363  ltleap  7373  nn1m1nn  7673  elnnz  7991  zletric  8025  zlelttric  8026  zmulcl  8033  zdceq  8052  zdcle  8053  zdclt  8054  ltpnf  8432  xrlttri3  8448  fzdcel  8634  bj-nn0suc0  9338