Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-axtd | Structured version Visualization version Unicode version |
Description: This implication, proved from propositional calculus only (hence holding, up to the standard interpretation, in any modal logic), shows that the axiom scheme (modal T) implies the axiom scheme (modal D). See also bj-axdd2 32576 and bj-axd2d 32577. (Contributed by BJ, 16-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
bj-axtd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con2 130 | . . 3 | |
2 | df-ex 1705 | . . 3 | |
3 | 1, 2 | syl6ibr 242 | . 2 |
4 | 3 | imim2d 57 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wal 1481 wex 1704 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-ex 1705 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |