Theorem renicax 1462

Description: A rederivation of nic-ax 1438 from lukshef-ax1 1459, proving that lukshef-ax1 1459 with nic-mp 1436 can be used as a complete axiomatization of propositional calculus. (Contributed by Anthony Hart, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
renicax	⊢ ((φ ⊼ (χ ⊼ ψ)) ⊼ ((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))))

Proof of Theorem renicax

Step	Hyp	Ref	Expression
1		lukshefth1 1460	. . . 4 ⊢ ((((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))) ⊼ (τ ⊼ (τ ⊼ τ))) ⊼ (φ ⊼ (χ ⊼ ψ)))
2		lukshefth2 1461	. . . 4 ⊢ (((((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))) ⊼ (τ ⊼ (τ ⊼ τ))) ⊼ (φ ⊼ (χ ⊼ ψ))) ⊼ (((φ ⊼ (χ ⊼ ψ)) ⊼ (((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))) ⊼ (τ ⊼ (τ ⊼ τ)))) ⊼ ((φ ⊼ (χ ⊼ ψ)) ⊼ (((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))) ⊼ (τ ⊼ (τ ⊼ τ))))))
3	1, 2	nic-mp 1436	. . 3 ⊢ ((φ ⊼ (χ ⊼ ψ)) ⊼ (((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))) ⊼ (τ ⊼ (τ ⊼ τ))))
4		lukshefth2 1461	. . . 4 ⊢ (((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))) ⊼ ((((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))) ⊼ (τ ⊼ (τ ⊼ τ))) ⊼ (((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))) ⊼ (τ ⊼ (τ ⊼ τ)))))
5		lukshef-ax1 1459	. . . 4 ⊢ ((((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))) ⊼ ((((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))) ⊼ (τ ⊼ (τ ⊼ τ))) ⊼ (((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))) ⊼ (τ ⊼ (τ ⊼ τ))))) ⊼ (((φ ⊼ (χ ⊼ ψ)) ⊼ ((φ ⊼ (χ ⊼ ψ)) ⊼ (φ ⊼ (χ ⊼ ψ)))) ⊼ (((φ ⊼ (χ ⊼ ψ)) ⊼ (((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))) ⊼ (τ ⊼ (τ ⊼ τ)))) ⊼ ((((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))) ⊼ (φ ⊼ (χ ⊼ ψ))) ⊼ (((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))) ⊼ (φ ⊼ (χ ⊼ ψ)))))))
6	4, 5	nic-mp 1436	. . 3 ⊢ (((φ ⊼ (χ ⊼ ψ)) ⊼ (((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))) ⊼ (τ ⊼ (τ ⊼ τ)))) ⊼ ((((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))) ⊼ (φ ⊼ (χ ⊼ ψ))) ⊼ (((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))) ⊼ (φ ⊼ (χ ⊼ ψ)))))
7	3, 6	nic-mp 1436	. 2 ⊢ (((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))) ⊼ (φ ⊼ (χ ⊼ ψ)))
8		lukshefth2 1461	. 2 ⊢ ((((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))) ⊼ (φ ⊼ (χ ⊼ ψ))) ⊼ (((φ ⊼ (χ ⊼ ψ)) ⊼ ((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))))) ⊼ ((φ ⊼ (χ ⊼ ψ)) ⊼ ((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))))))
9	7, 8	nic-mp 1436	1 ⊢ ((φ ⊼ (χ ⊼ ψ)) ⊼ ((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))))

This proof depends on syntax axioms:   ⊼ wnan 1287

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-an 360  df-nan 1288

This theorem is used by: (None)