Metamath Proof Explorer


Theorem re1luk3

Description: luk-3 derived from the Tarski-Bernays-Wajsberg axioms.

This theorem, along with re1luk1 and re1luk2 proves that tbw-ax1 , tbw-ax2 , tbw-ax3 , and tbw-ax4 , with ax-mp can be used as a complete axiom system for all of propositional calculus. (Contributed by Anthony Hart, 16-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion re1luk3 φ ¬ φ ψ

Proof

Step Hyp Ref Expression
1 tbw-negdf ¬ φ φ φ ¬ φ
2 tbwlem5 ¬ φ φ φ ¬ φ ¬ φ φ
3 1 2 ax-mp ¬ φ φ
4 tbw-ax4 ψ
5 tbw-ax1 φ ψ φ ψ
6 tbwlem1 φ ψ φ ψ ψ φ φ ψ
7 5 6 ax-mp ψ φ φ ψ
8 4 7 ax-mp φ φ ψ
9 tbwlem1 φ φ ψ φ φ ψ
10 8 9 ax-mp φ φ ψ
11 tbw-ax1 ¬ φ φ φ ψ ¬ φ ψ
12 3 10 11 mpsyl φ ¬ φ ψ