Theorem rblem4

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
Hypotheses	rblem4.1	⊢ ( ¬ 𝜑 ∨ 𝜃 )
	rblem4.2	⊢ ( ¬ 𝜓 ∨ 𝜏 )
	rblem4.3	⊢ ( ¬ 𝜒 ∨ 𝜂 )
Assertion	rblem4	⊢ ( ¬ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) ∨ ( ( 𝜂 ∨ 𝜏 ) ∨ 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		rblem4.1	⊢ ( ¬ 𝜑 ∨ 𝜃 )
2		rblem4.2	⊢ ( ¬ 𝜓 ∨ 𝜏 )
3		rblem4.3	⊢ ( ¬ 𝜒 ∨ 𝜂 )
4	3 2	rblem1	⊢ ( ¬ ( 𝜒 ∨ 𝜓 ) ∨ ( 𝜂 ∨ 𝜏 ) )
5	4 1	rblem1	⊢ ( ¬ ( ( 𝜒 ∨ 𝜓 ) ∨ 𝜑 ) ∨ ( ( 𝜂 ∨ 𝜏 ) ∨ 𝜃 ) )
6		rb-ax2	⊢ ( ¬ ( 𝜑 ∨ ( 𝜒 ∨ 𝜓 ) ) ∨ ( ( 𝜒 ∨ 𝜓 ) ∨ 𝜑 ) )
7		rb-ax2	⊢ ( ¬ ( 𝜓 ∨ 𝜒 ) ∨ ( 𝜒 ∨ 𝜓 ) )
8		rb-ax1	⊢ ( ¬ ( ¬ ( 𝜓 ∨ 𝜒 ) ∨ ( 𝜒 ∨ 𝜓 ) ) ∨ ( ¬ ( 𝜑 ∨ ( 𝜓 ∨ 𝜒 ) ) ∨ ( 𝜑 ∨ ( 𝜒 ∨ 𝜓 ) ) ) )
9	7 8	anmp	⊢ ( ¬ ( 𝜑 ∨ ( 𝜓 ∨ 𝜒 ) ) ∨ ( 𝜑 ∨ ( 𝜒 ∨ 𝜓 ) ) )
10		rb-ax2	⊢ ( ¬ ( ( 𝜓 ∨ 𝜒 ) ∨ 𝜑 ) ∨ ( 𝜑 ∨ ( 𝜓 ∨ 𝜒 ) ) )
11	9 10	rbsyl	⊢ ( ¬ ( ( 𝜓 ∨ 𝜒 ) ∨ 𝜑 ) ∨ ( 𝜑 ∨ ( 𝜒 ∨ 𝜓 ) ) )
12	6 11	rbsyl	⊢ ( ¬ ( ( 𝜓 ∨ 𝜒 ) ∨ 𝜑 ) ∨ ( ( 𝜒 ∨ 𝜓 ) ∨ 𝜑 ) )
13		rb-ax4	⊢ ( ¬ ( ( ( 𝜓 ∨ 𝜒 ) ∨ 𝜑 ) ∨ ( ( 𝜓 ∨ 𝜒 ) ∨ 𝜑 ) ) ∨ ( ( 𝜓 ∨ 𝜒 ) ∨ 𝜑 ) )
14		rb-ax2	⊢ ( ¬ ( 𝜑 ∨ ( 𝜓 ∨ 𝜒 ) ) ∨ ( ( 𝜓 ∨ 𝜒 ) ∨ 𝜑 ) )
15		rblem2	⊢ ( ¬ ( 𝜑 ∨ 𝜓 ) ∨ ( 𝜑 ∨ ( 𝜓 ∨ 𝜒 ) ) )
16	14 15	rbsyl	⊢ ( ¬ ( 𝜑 ∨ 𝜓 ) ∨ ( ( 𝜓 ∨ 𝜒 ) ∨ 𝜑 ) )
17		rb-ax3	⊢ ( ¬ 𝜒 ∨ ( 𝜓 ∨ 𝜒 ) )
18		rblem2	⊢ ( ¬ ( ¬ 𝜒 ∨ ( 𝜓 ∨ 𝜒 ) ) ∨ ( ¬ 𝜒 ∨ ( ( 𝜓 ∨ 𝜒 ) ∨ 𝜑 ) ) )
19	17 18	anmp	⊢ ( ¬ 𝜒 ∨ ( ( 𝜓 ∨ 𝜒 ) ∨ 𝜑 ) )
20	16 19	rblem1	⊢ ( ¬ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) ∨ ( ( ( 𝜓 ∨ 𝜒 ) ∨ 𝜑 ) ∨ ( ( 𝜓 ∨ 𝜒 ) ∨ 𝜑 ) ) )
21	13 20	rbsyl	⊢ ( ¬ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) ∨ ( ( 𝜓 ∨ 𝜒 ) ∨ 𝜑 ) )
22	12 21	rbsyl	⊢ ( ¬ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) ∨ ( ( 𝜒 ∨ 𝜓 ) ∨ 𝜑 ) )
23	5 22	rbsyl	⊢ ( ¬ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) ∨ ( ( 𝜂 ∨ 𝜏 ) ∨ 𝜃 ) )