Metamath Proof Explorer


Theorem rblem5

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

Ref Expression
Assertion rblem5 ¬¬¬φψ¬¬ψφ

Proof

Step Hyp Ref Expression
1 rb-ax2 ¬φ¬¬ψ¬¬ψφ
2 rb-ax4 ¬φφφ
3 rb-ax3 ¬φφφ
4 2 3 rbsyl ¬φφ
5 rb-ax4 ¬¬¬φ¬¬φ¬¬φ
6 rb-ax3 ¬¬¬φ¬¬φ¬¬φ
7 5 6 rbsyl ¬¬¬φ¬¬φ
8 rb-ax2 ¬¬¬¬φ¬¬φ¬¬φ¬¬¬φ
9 7 8 anmp ¬¬φ¬¬¬φ
10 9 4 rblem1 ¬¬φφ¬¬¬φφ
11 4 10 anmp ¬¬¬φφ
12 rb-ax4 ¬¬ψ¬ψ¬ψ
13 rb-ax3 ¬¬ψ¬ψ¬ψ
14 12 13 rbsyl ¬¬ψ¬ψ
15 rb-ax2 ¬¬¬ψ¬ψ¬ψ¬¬ψ
16 14 15 anmp ¬ψ¬¬ψ
17 11 16 rblem1 ¬¬¬φψφ¬¬ψ
18 1 17 rbsyl ¬¬¬φψ¬¬ψφ