Theorem orc 633

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

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

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

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm2.67-2  634  pm1.4  646  orci  650  orcd  652  orcs  654  pm2.45  657  biorfi  665  pm1.5  682  pm2.4  695  pm4.44  696  pm4.45  698  pm3.48  699  pm2.76  721  orabs  727  ordi  729  andi  731  pm4.72  736  biort  738  dcim  784  pm2.54dc  790  pm4.78i  808  pm2.85dc  811  dcor  843  pm5.71dc  868  dedlema  876  3mix1  1073  xoranor  1268  19.33  1373  hbor  1438  nford  1459  19.30dc  1518  19.43  1519  19.32r  1570  moor  1971  r19.32r  2457  ssun1  3106  undif3ss  3198  reuun1  3219  prmg  3489  opthpr  3543  issod  4056  elelsuc  4146  ordtri2or2exmidlem  4251  regexmidlem1  4258  nndceq  6077  nndcel  6078  swoord1  6135  swoord2  6136  addlocprlem  6633  msqge0  7607  mulge0  7610  ltleap  7621  nn1m1nn  7932  elnnz  8255  zletric  8289  zlelttric  8290  zmulcl  8297  zdceq  8316  zdcle  8317  zdclt  8318  ltpnf  8702  xrlttri3  8718  fzdcel  8904  qletric  9099  qlelttric  9100  qdceq  9102  bj-nn0suc0  10075