modal-5 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > modal-5		Structured version Visualization version Unicode version

Theorem modal-5 2032

Description: The analogue in our predicate calculus of axiom (5) of modal logic S5. (Contributed by NM, 5-Oct-2005.)

**Assertion**
Ref	Expression
modal-5

**Proof of Theorem modal-5**
Step	Hyp	Ref	Expression
1		hbn1 2020	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wal 1481

This theorem was proved from axioms: ax-10 2019

This theorem is referenced by: (None)