Metamath Proof Explorer

Theorem rb-ax4

Description: 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.)

Ref Expression
Assertion rb-ax4 ¬ φ φ φ


Step Hyp Ref Expression
1 pm1.2 φ φ φ
2 1 con3i ¬ φ ¬ φ φ
3 2 con1i ¬ ¬ φ φ φ
4 3 orri ¬ φ φ φ