Metamath Proof Explorer


Theorem rblem3

Description: Used to rederive the Lukasiewicz axioms from Russell-Bernays'. (Contributed by Anthony Hart, 18-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion rblem3 ¬ χ φ χ ψ φ

Proof

Step Hyp Ref Expression
1 rb-ax2 ¬ φ χ ψ χ ψ φ
2 rblem2 ¬ φ χ φ χ ψ
3 rb-ax2 ¬ χ φ φ χ
4 2 3 rbsyl ¬ χ φ φ χ ψ
5 1 4 rbsyl ¬ χ φ χ ψ φ