This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bj-modal4

Description: First-order logic form of the modal axiom (4). See hba1 . This is the standard proof of the implication in modal logic (B5 => 4). Its dual statement is bj-modal4e . (Contributed by BJ, 12-Aug-2023) (Proof modification is discouraged.)

Ref Expression
Assertion bj-modal4 ⊢ ∀ x φ → ∀ x ∀ x φ

Proof

Step Hyp Ref Expression
1 bj-modalbe ⊢ ∀ x φ → ∀ x ∃ x ∀ x φ
2 hbe1a ⊢ ∃ x ∀ x φ → ∀ x φ
3 1 2 sylg ⊢ ∀ x φ → ∀ x ∀ x φ