Metamath Proof Explorer

Theorem nfimd

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 ) )`

Proof

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 ) )`