Description: Nonfreeness in the antecedent and the consequent of an implication implies nonfreeness in the implication, deduction form. (Contributed by BJ, 2-Dec-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bj-nnfimd.1 | |- ( ph -> F// x ps ) |
|
bj-nnfimd.2 | |- ( ph -> F// x ch ) |
||
Assertion | bj-nnfimd | |- ( ph -> F// x ( ps -> ch ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-nnfimd.1 | |- ( ph -> F// x ps ) |
|
2 | bj-nnfimd.2 | |- ( ph -> F// x ch ) |
|
3 | bj-nnfim | |- ( ( F// x ps /\ F// x ch ) -> F// x ( ps -> ch ) ) |
|
4 | 1 2 3 | syl2anc | |- ( ph -> F// x ( ps -> ch ) ) |