bj-gl4 - Mathbox for BJ

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

Theorem bj-gl4 32580

Description: In a normal modal logic, the modal axiom GL implies the modal axiom (4). Note that the antecedent of bj-gl4 32580 is an instance of the axiom GL, with

replaced by

$/\$

, sometimes called the "strong necessity" of

. (Contributed by BJ, 12-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.)

**Assertion**
Ref	Expression
bj-gl4	$/\$ $/\$ $/\$

**Proof of Theorem bj-gl4**
Step	Hyp	Ref	Expression
1		bj-gl4lem 32579	. . 3 $/\$ $/\$
2		19.26 1798	. . . 4 $/\$ $/\$
3	2	biimpi 206	. . 3 $/\$ $/\$
4	1, 3	imim12i 62	. 2 $/\$ $/\$ $/\$ $/\$
5		simpl 473	. 2 $/\$
6	4, 5	syl6 35	1 $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 384

wal 1481

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737

This theorem depends on definitions: df-bi 197 df-an 386

This theorem is referenced by: (None)

W3C validator