bj-modald - Mathbox for BJ

	Mathbox for BJ		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-modald		Structured version Visualization version Unicode version

Theorem bj-modald 32661

Description: A short form of the axiom D of modal logic. (Contributed by BJ, 4-Apr-2021.)

**Assertion**
Ref	Expression
bj-modald

**Proof of Theorem bj-modald**
Step	Hyp	Ref	Expression
1		19.2 1892	. . 3
2		df-ex 1705	. . 3
3	1, 2	sylib 208	. 2
4	3	con2i 134	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 ax-gen 1722 ax-4 1737 ax-6 1888

This theorem depends on definitions: df-bi 197 df-ex 1705

This theorem is referenced by: (None)