modal-5 - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > modal-5		Unicode version

Theorem modal-5 1733

Description: The analog in our "pure" 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 1730	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wal 1540

This theorem was proved from axioms: ax-6 1729

This theorem is referenced by: (None)