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 ψ


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