Theorem olc 373

Description: Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.)

Assertion

Ref	Expression
olc	|- (ph -> (ps \/ ph))

Proof of Theorem olc

Step	Hyp	Ref	Expression
1		ax-1 6	. 2 |- (ph -> (-. ps -> ph))
2	1	orrd 367	1 |- (ph -> (ps \/ ph))

Syntax hints:  -. wn 3   -> 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  pm2.07  385  pm2.46  387  biorf  394  pm1.5  508  pm2.41  556  jaob  758  pm3.48  806  andi  837  pm4.72  846  dedlemb  921  consensus  925  cad1  1398  19.33  1607  19.33b  1608  dfsb2  2055  mooran2  2259  euor2  2272  undif3  3516  undif4  3608  phiall  4619  leconnnc  6219  ncslesuc  6268