Theorem rblem6 1527

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

Hypothesis

Ref	Expression
rblem6.1	⊢ ¬ (¬ (¬ φ ∨ ψ) ∨ ¬ (¬ ψ ∨ φ))

Assertion

Ref	Expression
rblem6	⊢ (¬ φ ∨ ψ)

Proof of Theorem rblem6

Step	Hyp	Ref	Expression
1		rblem6.1	. 2 ⊢ ¬ (¬ (¬ φ ∨ ψ) ∨ ¬ (¬ ψ ∨ φ))
2		rb-ax4 1520	. . . . . . 7 ⊢ (¬ (¬ (¬ φ ∨ ψ) ∨ ¬ (¬ φ ∨ ψ)) ∨ ¬ (¬ φ ∨ ψ))
3		rb-ax3 1519	. . . . . . 7 ⊢ (¬ ¬ (¬ φ ∨ ψ) ∨ (¬ (¬ φ ∨ ψ) ∨ ¬ (¬ φ ∨ ψ)))
4	2, 3	rbsyl 1521	. . . . . 6 ⊢ (¬ ¬ (¬ φ ∨ ψ) ∨ ¬ (¬ φ ∨ ψ))
5		rb-ax2 1518	. . . . . 6 ⊢ (¬ (¬ ¬ (¬ φ ∨ ψ) ∨ ¬ (¬ φ ∨ ψ)) ∨ (¬ (¬ φ ∨ ψ) ∨ ¬ ¬ (¬ φ ∨ ψ)))
6	4, 5	anmp 1516	. . . . 5 ⊢ (¬ (¬ φ ∨ ψ) ∨ ¬ ¬ (¬ φ ∨ ψ))
7		rblem3 1524	. . . . 5 ⊢ (¬ (¬ (¬ φ ∨ ψ) ∨ ¬ ¬ (¬ φ ∨ ψ)) ∨ ((¬ (¬ φ ∨ ψ) ∨ ¬ (¬ ψ ∨ φ)) ∨ ¬ ¬ (¬ φ ∨ ψ)))
8	6, 7	anmp 1516	. . . 4 ⊢ ((¬ (¬ φ ∨ ψ) ∨ ¬ (¬ ψ ∨ φ)) ∨ ¬ ¬ (¬ φ ∨ ψ))
9		rb-ax2 1518	. . . 4 ⊢ (¬ ((¬ (¬ φ ∨ ψ) ∨ ¬ (¬ ψ ∨ φ)) ∨ ¬ ¬ (¬ φ ∨ ψ)) ∨ (¬ ¬ (¬ φ ∨ ψ) ∨ (¬ (¬ φ ∨ ψ) ∨ ¬ (¬ ψ ∨ φ))))
10	8, 9	anmp 1516	. . 3 ⊢ (¬ ¬ (¬ φ ∨ ψ) ∨ (¬ (¬ φ ∨ ψ) ∨ ¬ (¬ ψ ∨ φ)))
11		rblem5 1526	. . 3 ⊢ (¬ (¬ ¬ (¬ φ ∨ ψ) ∨ (¬ (¬ φ ∨ ψ) ∨ ¬ (¬ ψ ∨ φ))) ∨ (¬ ¬ (¬ (¬ φ ∨ ψ) ∨ ¬ (¬ ψ ∨ φ)) ∨ (¬ φ ∨ ψ)))
12	10, 11	anmp 1516	. 2 ⊢ (¬ ¬ (¬ (¬ φ ∨ ψ) ∨ ¬ (¬ ψ ∨ φ)) ∨ (¬ φ ∨ ψ))
13	1, 12	anmp 1516	1 ⊢ (¬ φ ∨ ψ)

Syntax hints:  ¬ wn 3   ∨ wo 357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

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

This theorem is referenced by:  re1axmp  1529  re2luk1  1530  re2luk2  1531