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

Metamath Proof Explorer

Theorem bj-nnf-alrim

Description: Proof of the closed form of alrimi from modalK (compare alrimiv ). See also bj-alrim . Actually, most proofs between 19.3t and 2sbbid could be proved without ax-12 . (Contributed by BJ, 20-Aug-2023)

Ref Expression
Assertion bj-nnf-alrim ⊢ Ⅎ' x φ → ∀ x φ → ψ → φ → ∀ x ψ

Proof

Step Hyp Ref Expression
1 bj-nnfa ⊢ Ⅎ' x φ → φ → ∀ x φ
2 alim ⊢ ∀ x φ → ψ → ∀ x φ → ∀ x ψ
3 1 2 syl9 ⊢ Ⅎ' x φ → ∀ x φ → ψ → φ → ∀ x ψ