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 | ⊢ ( 𝜑 → ( ¬ 𝜑 → 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tbw-ax4 | ⊢ ( ⊥ → 𝜓 ) | |
| 2 | tbw-ax1 | ⊢ ( ( 𝜑 → ⊥ ) → ( ( ⊥ → 𝜓 ) → ( 𝜑 → 𝜓 ) ) ) | |
| 3 | tbwlem1 | ⊢ ( ( ( 𝜑 → ⊥ ) → ( ( ⊥ → 𝜓 ) → ( 𝜑 → 𝜓 ) ) ) → ( ( ⊥ → 𝜓 ) → ( ( 𝜑 → ⊥ ) → ( 𝜑 → 𝜓 ) ) ) ) | |
| 4 | 2 3 | ax-mp | ⊢ ( ( ⊥ → 𝜓 ) → ( ( 𝜑 → ⊥ ) → ( 𝜑 → 𝜓 ) ) ) |
| 5 | 1 4 | ax-mp | ⊢ ( ( 𝜑 → ⊥ ) → ( 𝜑 → 𝜓 ) ) |
| 6 | tbwlem1 | ⊢ ( ( ( 𝜑 → ⊥ ) → ( 𝜑 → 𝜓 ) ) → ( 𝜑 → ( ( 𝜑 → ⊥ ) → 𝜓 ) ) ) | |
| 7 | 5 6 | ax-mp | ⊢ ( 𝜑 → ( ( 𝜑 → ⊥ ) → 𝜓 ) ) |
| 8 | tbw-negdf | ⊢ ( ( ( ¬ 𝜑 → ( 𝜑 → ⊥ ) ) → ( ( ( 𝜑 → ⊥ ) → ¬ 𝜑 ) → ⊥ ) ) → ⊥ ) | |
| 9 | tbwlem5 | ⊢ ( ( ( ( ¬ 𝜑 → ( 𝜑 → ⊥ ) ) → ( ( ( 𝜑 → ⊥ ) → ¬ 𝜑 ) → ⊥ ) ) → ⊥ ) → ( ¬ 𝜑 → ( 𝜑 → ⊥ ) ) ) | |
| 10 | 8 9 | ax-mp | ⊢ ( ¬ 𝜑 → ( 𝜑 → ⊥ ) ) |
| 11 | tbw-ax1 | ⊢ ( ( ¬ 𝜑 → ( 𝜑 → ⊥ ) ) → ( ( ( 𝜑 → ⊥ ) → 𝜓 ) → ( ¬ 𝜑 → 𝜓 ) ) ) | |
| 12 | 10 11 | ax-mp | ⊢ ( ( ( 𝜑 → ⊥ ) → 𝜓 ) → ( ¬ 𝜑 → 𝜓 ) ) |
| 13 | 7 12 | tbwsyl | ⊢ ( 𝜑 → ( ¬ 𝜑 → 𝜓 ) ) |