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 | |- ( ph -> ( -. ph -> ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tbw-negdf | |- ( ( ( -. ph -> ( ph -> F. ) ) -> ( ( ( ph -> F. ) -> -. ph ) -> F. ) ) -> F. ) |
|
| 2 | tbwlem5 | |- ( ( ( ( -. ph -> ( ph -> F. ) ) -> ( ( ( ph -> F. ) -> -. ph ) -> F. ) ) -> F. ) -> ( -. ph -> ( ph -> F. ) ) ) |
|
| 3 | 1 2 | ax-mp | |- ( -. ph -> ( ph -> F. ) ) |
| 4 | tbw-ax4 | |- ( F. -> ps ) |
|
| 5 | tbw-ax1 | |- ( ( ph -> F. ) -> ( ( F. -> ps ) -> ( ph -> ps ) ) ) |
|
| 6 | tbwlem1 | |- ( ( ( ph -> F. ) -> ( ( F. -> ps ) -> ( ph -> ps ) ) ) -> ( ( F. -> ps ) -> ( ( ph -> F. ) -> ( ph -> ps ) ) ) ) |
|
| 7 | 5 6 | ax-mp | |- ( ( F. -> ps ) -> ( ( ph -> F. ) -> ( ph -> ps ) ) ) |
| 8 | 4 7 | ax-mp | |- ( ( ph -> F. ) -> ( ph -> ps ) ) |
| 9 | tbwlem1 | |- ( ( ( ph -> F. ) -> ( ph -> ps ) ) -> ( ph -> ( ( ph -> F. ) -> ps ) ) ) |
|
| 10 | 8 9 | ax-mp | |- ( ph -> ( ( ph -> F. ) -> ps ) ) |
| 11 | tbw-ax1 | |- ( ( -. ph -> ( ph -> F. ) ) -> ( ( ( ph -> F. ) -> ps ) -> ( -. ph -> ps ) ) ) |
|
| 12 | 3 10 11 | mpsyl | |- ( ph -> ( -. ph -> ps ) ) |