Description: tbw-ax4 rederived from merco2 .
This theorem, along with re1tbw1 , re1tbw2 , and re1tbw3 , shows that merco2 , along with ax-mp , can be used as a complete axiomatization of propositional calculus. (Contributed by Anthony Hart, 16-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | re1tbw4 | ⊢ ( ⊥ → 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | re1tbw3 | ⊢ ( ( ( 𝜑 → 𝜑 ) → 𝜑 ) → 𝜑 ) | |
| 2 | re1tbw2 | ⊢ ( 𝜑 → ( ( 𝜑 → 𝜑 ) → 𝜑 ) ) | |
| 3 | re1tbw1 | ⊢ ( ( 𝜑 → ( ( 𝜑 → 𝜑 ) → 𝜑 ) ) → ( ( ( ( 𝜑 → 𝜑 ) → 𝜑 ) → 𝜑 ) → ( 𝜑 → 𝜑 ) ) ) | |
| 4 | 2 3 | ax-mp | ⊢ ( ( ( ( 𝜑 → 𝜑 ) → 𝜑 ) → 𝜑 ) → ( 𝜑 → 𝜑 ) ) |
| 5 | 1 4 | ax-mp | ⊢ ( 𝜑 → 𝜑 ) |
| 6 | re1tbw3 | ⊢ ( ( ( ( ⊥ → 𝜑 ) → 𝜑 ) → ( ⊥ → 𝜑 ) ) → ( ⊥ → 𝜑 ) ) | |
| 7 | re1tbw2 | ⊢ ( ( ⊥ → 𝜑 ) → ( ( ( ⊥ → 𝜑 ) → 𝜑 ) → ( ⊥ → 𝜑 ) ) ) | |
| 8 | re1tbw1 | ⊢ ( ( ( ⊥ → 𝜑 ) → ( ( ( ⊥ → 𝜑 ) → 𝜑 ) → ( ⊥ → 𝜑 ) ) ) → ( ( ( ( ( ⊥ → 𝜑 ) → 𝜑 ) → ( ⊥ → 𝜑 ) ) → ( ⊥ → 𝜑 ) ) → ( ( ⊥ → 𝜑 ) → ( ⊥ → 𝜑 ) ) ) ) | |
| 9 | 7 8 | ax-mp | ⊢ ( ( ( ( ( ⊥ → 𝜑 ) → 𝜑 ) → ( ⊥ → 𝜑 ) ) → ( ⊥ → 𝜑 ) ) → ( ( ⊥ → 𝜑 ) → ( ⊥ → 𝜑 ) ) ) |
| 10 | 6 9 | ax-mp | ⊢ ( ( ⊥ → 𝜑 ) → ( ⊥ → 𝜑 ) ) |
| 11 | mercolem3 | ⊢ ( ( ( ⊥ → 𝜑 ) → 𝜑 ) → ( ( ⊥ → 𝜑 ) → ( ⊥ → 𝜑 ) ) ) | |
| 12 | merco2 | ⊢ ( ( ( ( ⊥ → 𝜑 ) → 𝜑 ) → ( ( ⊥ → 𝜑 ) → ( ⊥ → 𝜑 ) ) ) → ( ( ( ⊥ → 𝜑 ) → ( ⊥ → 𝜑 ) ) → ( ( 𝜑 → 𝜑 ) → ( ( 𝜑 → 𝜑 ) → ( ⊥ → 𝜑 ) ) ) ) ) | |
| 13 | 11 12 | ax-mp | ⊢ ( ( ( ⊥ → 𝜑 ) → ( ⊥ → 𝜑 ) ) → ( ( 𝜑 → 𝜑 ) → ( ( 𝜑 → 𝜑 ) → ( ⊥ → 𝜑 ) ) ) ) |
| 14 | 10 13 | ax-mp | ⊢ ( ( 𝜑 → 𝜑 ) → ( ( 𝜑 → 𝜑 ) → ( ⊥ → 𝜑 ) ) ) |
| 15 | 5 14 | ax-mp | ⊢ ( ( 𝜑 → 𝜑 ) → ( ⊥ → 𝜑 ) ) |
| 16 | 5 15 | ax-mp | ⊢ ( ⊥ → 𝜑 ) |