Metamath Proof Explorer

Theorem bj-gl4

Description: In a normal modal logic, the modal axiom GL implies the modal axiom (4). Translated to first-order logic, Axiom GL reads |- ( A. x ( A. x ph -> ph ) -> A. x ph ) . Note that the antecedent of bj-gl4 is an instance of the axiom GL, with ph replaced by ( A. x ph /\ ph ) , which is a modality sometimes called the "strong necessity" of ph . (Contributed by BJ, 12-Dec-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion bj-gl4 ⊢ ∀ x ∀ x ∀ x φ ∧ φ → ∀ x φ ∧ φ → ∀ x ∀ x φ ∧ φ → ∀ x φ → ∀ x ∀ x φ

Proof

Step Hyp Ref Expression
1 19.26 ⊢ ∀ x ∀ x φ ∧ φ ↔ ∀ x ∀ x φ ∧ ∀ x φ
2 simpr ⊢ ∀ x ∀ x φ ∧ ∀ x φ → ∀ x φ
3 2 a1i ⊢ φ → ∀ x ∀ x φ ∧ ∀ x φ → ∀ x φ
4 3 anc2ri ⊢ φ → ∀ x ∀ x φ ∧ ∀ x φ → ∀ x φ ∧ φ
5 1 4 biimtrid ⊢ φ → ∀ x ∀ x φ ∧ φ → ∀ x φ ∧ φ
6 5 alimi ⊢ ∀ x φ → ∀ x ∀ x ∀ x φ ∧ φ → ∀ x φ ∧ φ
7 1 biimpi ⊢ ∀ x ∀ x φ ∧ φ → ∀ x ∀ x φ ∧ ∀ x φ
8 6 7 imim12i ⊢ ∀ x ∀ x ∀ x φ ∧ φ → ∀ x φ ∧ φ → ∀ x ∀ x φ ∧ φ → ∀ x φ → ∀ x ∀ x φ ∧ ∀ x φ
9 simpl ⊢ ∀ x ∀ x φ ∧ ∀ x φ → ∀ x ∀ x φ
10 8 9 syl6 ⊢ ∀ x ∀ x ∀ x φ ∧ φ → ∀ x φ ∧ φ → ∀ x ∀ x φ ∧ φ → ∀ x φ → ∀ x ∀ x φ