Description: If in a context x is not free in ps and ch , then it is not free in ( ps -> ch ) . Deduction form of nfim . (Contributed by Mario Carneiro, 24-Sep-2016) (Proof shortened by Wolf Lammen, 30-Dec-2017) df-nf changed. (Revised by Wolf Lammen, 18-Sep-2021) Eliminate curried form of nfimt . (Revised by Wolf Lammen, 10-Jul-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nfimd.1 | |- ( ph -> F/ x ps ) |
|
| nfimd.2 | |- ( ph -> F/ x ch ) |
||
| Assertion | nfimd | |- ( ph -> F/ x ( ps -> ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfimd.1 | |- ( ph -> F/ x ps ) |
|
| 2 | nfimd.2 | |- ( ph -> F/ x ch ) |
|
| 3 | 19.35 | |- ( E. x ( ps -> ch ) <-> ( A. x ps -> E. x ch ) ) |
|
| 4 | 3 | biimpi | |- ( E. x ( ps -> ch ) -> ( A. x ps -> E. x ch ) ) |
| 5 | 1 | nfrd | |- ( ph -> ( E. x ps -> A. x ps ) ) |
| 6 | 2 | nfrd | |- ( ph -> ( E. x ch -> A. x ch ) ) |
| 7 | 5 6 | imim12d | |- ( ph -> ( ( A. x ps -> E. x ch ) -> ( E. x ps -> A. x ch ) ) ) |
| 8 | 19.38 | |- ( ( E. x ps -> A. x ch ) -> A. x ( ps -> ch ) ) |
|
| 9 | 4 7 8 | syl56 | |- ( ph -> ( E. x ( ps -> ch ) -> A. x ( ps -> ch ) ) ) |
| 10 | 9 | nfd | |- ( ph -> F/ x ( ps -> ch ) ) |