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	⊢ ( ¬ ( ¬ ¬ 𝜑 ∨ 𝜓 ) ∨ ( ¬ ¬ 𝜓 ∨ 𝜑 ) )