Theorem rb-ax4 14222

Description: The fourth of four axioms in the Russell-Bernays axiom system.

Assertion

Ref	Expression
rb-ax4	|- (-. (ph \/ ph) \/ ph)

Proof of Theorem rb-ax4

Step	Hyp	Ref	Expression
1		pm1.2 265	. . . 4 |- ((ph \/ ph) -> ph)
2	1	con3i 114	. . 3 |- (-. ph -> -. (ph \/ ph))
3	2	con1i 112	. 2 |- (-. -. (ph \/ ph) -> ph)
4	3	orri 248	1 |- (-. (ph \/ ph) \/ ph)

Syntax hints:  -. wn 2   \/ wo 239

This theorem is referenced by:  rblem4 14227  rblem5 14228  rblem6 14229  re2luk1 14232  re2luk2 14233  re2luk3 14234

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

This theorem depends on definitions:  df-bi 164  df-or 241

Copyright terms: Public domain