Description: If two formulas are equivalent for all x , then nonfreeness of x in one of them is equivalent to nonfreeness in the other, inference form. See bj-nnfbi . (Contributed by BJ, 18-Nov-2023)
Ref | Expression | ||
---|---|---|---|
Hypothesis | bj-nnfbii.1 | |- ( ph <-> ps ) |
|
Assertion | bj-nnfbii | |- ( F// x ph <-> F// x ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-nnfbii.1 | |- ( ph <-> ps ) |
|
2 | bj-nnfbi | |- ( ( ( ph <-> ps ) /\ A. x ( ph <-> ps ) ) -> ( F// x ph <-> F// x ps ) ) |
|
3 | 1 2 | bj-mpgs | |- ( F// x ph <-> F// x ps ) |