Metamath Proof Explorer


Theorem rblem6

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
Hypothesis rblem6.1 ¬ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ( ¬ 𝜓𝜑 ) )
Assertion rblem6 ( ¬ 𝜑𝜓 )

Proof

Step Hyp Ref Expression
1 rblem6.1 ¬ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ( ¬ 𝜓𝜑 ) )
2 rb-ax4 ( ¬ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ( ¬ 𝜑𝜓 ) ) ∨ ¬ ( ¬ 𝜑𝜓 ) )
3 rb-ax3 ( ¬ ¬ ( ¬ 𝜑𝜓 ) ∨ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ( ¬ 𝜑𝜓 ) ) )
4 2 3 rbsyl ( ¬ ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ( ¬ 𝜑𝜓 ) )
5 rb-ax2 ( ¬ ( ¬ ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ( ¬ 𝜑𝜓 ) ) ∨ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ¬ ( ¬ 𝜑𝜓 ) ) )
6 4 5 anmp ( ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ¬ ( ¬ 𝜑𝜓 ) )
7 rblem3 ( ¬ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ¬ ( ¬ 𝜑𝜓 ) ) ∨ ( ( ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ( ¬ 𝜓𝜑 ) ) ∨ ¬ ¬ ( ¬ 𝜑𝜓 ) ) )
8 6 7 anmp ( ( ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ( ¬ 𝜓𝜑 ) ) ∨ ¬ ¬ ( ¬ 𝜑𝜓 ) )
9 rb-ax2 ( ¬ ( ( ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ( ¬ 𝜓𝜑 ) ) ∨ ¬ ¬ ( ¬ 𝜑𝜓 ) ) ∨ ( ¬ ¬ ( ¬ 𝜑𝜓 ) ∨ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ( ¬ 𝜓𝜑 ) ) ) )
10 8 9 anmp ( ¬ ¬ ( ¬ 𝜑𝜓 ) ∨ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ( ¬ 𝜓𝜑 ) ) )
11 rblem5 ( ¬ ( ¬ ¬ ( ¬ 𝜑𝜓 ) ∨ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ( ¬ 𝜓𝜑 ) ) ) ∨ ( ¬ ¬ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ( ¬ 𝜓𝜑 ) ) ∨ ( ¬ 𝜑𝜓 ) ) )
12 10 11 anmp ( ¬ ¬ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ¬ ( ¬ 𝜓𝜑 ) ) ∨ ( ¬ 𝜑𝜓 ) )
13 1 12 anmp ( ¬ 𝜑𝜓 )