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	⊢ (¬ ∀x ¬ φ → ∀x ¬ ∀x ¬ φ)

Proof of Theorem modal-5

Step	Hyp	Ref	Expression
1		hbn1 1730	1 ⊢ (¬ ∀x ¬ φ → ∀x ¬ ∀x ¬ φ)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1540

This proof depends on axioms:  ax-6 1729

This theorem is used by: (None)