Theorem orc 374

Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.)

Assertion

Ref	Expression
orc	⊢ (φ → (φ ∨ ψ))

Proof of Theorem orc

Step	Hyp	Ref	Expression
1		pm2.24 101	. 2 ⊢ (φ → (¬ φ → ψ))
2	1	orrd 367	1 ⊢ (φ → (φ ∨ ψ))

Syntax hints:   → wi 4   ∨ wo 357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-or 359

This theorem is referenced by:  pm1.4  375  orcd  381  orcs  383  pm2.45  386  pm2.67-2  391  biorfi  396  pm1.5  508  pm2.4  558  pm4.44  560  pm4.45  669  pm3.48  806  orabs  828  andi  837  pm4.72  846  biort  866  pm5.71  902  dedlema  920  consensus  925  3mix1  1124  cad1  1398  cad11  1399  cad0  1400  19.33  1607  19.33b  1608  dfsb2  2055  moor  2257  ssun1  3427  undif3  3516  reuun1  3538  phiall  4619  clos1basesuc  5883  leconnnc  6219  ncslesuc  6268  nchoicelem9  6298