Description: A variable is nonfree in a theorem. The antecedent is in the "strong necessity" modality of modal logic in order not to require sp (modal T), as in bj-nnfbi . (Contributed by BJ, 28-Jul-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-nnftht | |- ( ( ph /\ A. x ph ) -> F// x ph ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1 | |- ( ph -> ( E. x ph -> ph ) ) |
|
2 | ax-1 | |- ( A. x ph -> ( ph -> A. x ph ) ) |
|
3 | 1 2 | anim12i | |- ( ( ph /\ A. x ph ) -> ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) ) |
4 | df-bj-nnf | |- ( F// x ph <-> ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) ) |
|
5 | 3 4 | sylibr | |- ( ( ph /\ A. x ph ) -> F// x ph ) |