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 | |- ( F// x ph -> ( A. x ( ph -> ps ) -> ( ph -> A. x ps ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-nnfa | |- ( F// x ph -> ( ph -> A. x ph ) ) |
|
| 2 | alim | |- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) ) |
|
| 3 | 1 2 | syl9 | |- ( F// x ph -> ( A. x ( ph -> ps ) -> ( ph -> A. x ps ) ) ) |