Theorem rblem4 1525

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.)

Hypotheses

Ref	Expression
rblem4.1	⊢ (¬ φ ∨ θ)
rblem4.2	⊢ (¬ ψ ∨ τ)
rblem4.3	⊢ (¬ χ ∨ η)

Assertion

Ref	Expression
rblem4	⊢ (¬ ((φ ∨ ψ) ∨ χ) ∨ ((η ∨ τ) ∨ θ))

Proof of Theorem rblem4

Step	Hyp	Ref	Expression
1		rblem4.3	. . . 4 ⊢ (¬ χ ∨ η)
2		rblem4.2	. . . 4 ⊢ (¬ ψ ∨ τ)
3	1, 2	rblem1 1522	. . 3 ⊢ (¬ (χ ∨ ψ) ∨ (η ∨ τ))
4		rblem4.1	. . 3 ⊢ (¬ φ ∨ θ)
5	3, 4	rblem1 1522	. 2 ⊢ (¬ ((χ ∨ ψ) ∨ φ) ∨ ((η ∨ τ) ∨ θ))
6		rb-ax2 1518	. . . 4 ⊢ (¬ (φ ∨ (χ ∨ ψ)) ∨ ((χ ∨ ψ) ∨ φ))
7		rb-ax2 1518	. . . . . 6 ⊢ (¬ (ψ ∨ χ) ∨ (χ ∨ ψ))
8		rb-ax1 1517	. . . . . 6 ⊢ (¬ (¬ (ψ ∨ χ) ∨ (χ ∨ ψ)) ∨ (¬ (φ ∨ (ψ ∨ χ)) ∨ (φ ∨ (χ ∨ ψ))))
9	7, 8	anmp 1516	. . . . 5 ⊢ (¬ (φ ∨ (ψ ∨ χ)) ∨ (φ ∨ (χ ∨ ψ)))
10		rb-ax2 1518	. . . . 5 ⊢ (¬ ((ψ ∨ χ) ∨ φ) ∨ (φ ∨ (ψ ∨ χ)))
11	9, 10	rbsyl 1521	. . . 4 ⊢ (¬ ((ψ ∨ χ) ∨ φ) ∨ (φ ∨ (χ ∨ ψ)))
12	6, 11	rbsyl 1521	. . 3 ⊢ (¬ ((ψ ∨ χ) ∨ φ) ∨ ((χ ∨ ψ) ∨ φ))
13		rb-ax4 1520	. . . 4 ⊢ (¬ (((ψ ∨ χ) ∨ φ) ∨ ((ψ ∨ χ) ∨ φ)) ∨ ((ψ ∨ χ) ∨ φ))
14		rb-ax2 1518	. . . . . 6 ⊢ (¬ (φ ∨ (ψ ∨ χ)) ∨ ((ψ ∨ χ) ∨ φ))
15		rblem2 1523	. . . . . 6 ⊢ (¬ (φ ∨ ψ) ∨ (φ ∨ (ψ ∨ χ)))
16	14, 15	rbsyl 1521	. . . . 5 ⊢ (¬ (φ ∨ ψ) ∨ ((ψ ∨ χ) ∨ φ))
17		rb-ax3 1519	. . . . . 6 ⊢ (¬ χ ∨ (ψ ∨ χ))
18		rblem2 1523	. . . . . 6 ⊢ (¬ (¬ χ ∨ (ψ ∨ χ)) ∨ (¬ χ ∨ ((ψ ∨ χ) ∨ φ)))
19	17, 18	anmp 1516	. . . . 5 ⊢ (¬ χ ∨ ((ψ ∨ χ) ∨ φ))
20	16, 19	rblem1 1522	. . . 4 ⊢ (¬ ((φ ∨ ψ) ∨ χ) ∨ (((ψ ∨ χ) ∨ φ) ∨ ((ψ ∨ χ) ∨ φ)))
21	13, 20	rbsyl 1521	. . 3 ⊢ (¬ ((φ ∨ ψ) ∨ χ) ∨ ((ψ ∨ χ) ∨ φ))
22	12, 21	rbsyl 1521	. 2 ⊢ (¬ ((φ ∨ ψ) ∨ χ) ∨ ((χ ∨ ψ) ∨ φ))
23	5, 22	rbsyl 1521	1 ⊢ (¬ ((φ ∨ ψ) ∨ χ) ∨ ((η ∨ τ) ∨ θ))

This proof depends on syntax axioms:  ¬ wn 3   ∨ wo 357

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 177  df-or 359  df-an 360

This theorem is used by:  re2luk1  1530