Description: A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-nnfim2 | |- ( ( F// x ph /\ F// x ps ) -> ( ( A. x ph -> E. x ps ) -> ( ph -> ps ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-nnfa | |- ( F// x ph -> ( ph -> A. x ph ) ) |
|
2 | bj-nnfe | |- ( F// x ps -> ( E. x ps -> ps ) ) |
|
3 | imim12 | |- ( ( ph -> A. x ph ) -> ( ( E. x ps -> ps ) -> ( ( A. x ph -> E. x ps ) -> ( ph -> ps ) ) ) ) |
|
4 | 3 | imp | |- ( ( ( ph -> A. x ph ) /\ ( E. x ps -> ps ) ) -> ( ( A. x ph -> E. x ps ) -> ( ph -> ps ) ) ) |
5 | 1 2 4 | syl2an | |- ( ( F// x ph /\ F// x ps ) -> ( ( A. x ph -> E. x ps ) -> ( ph -> ps ) ) ) |