Theorem rb-ax4

The fourth of four axioms in the Russell-Bernays axiom system. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \neg (\varphi \vee \varphi) \vee \varphi \)
Proof
pm1.2
con3i _
con1i _
orri _