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 φ x ψ
nfimd.2 φ x χ
Assertion nfimd φ x ψ χ

Proof

Step Hyp Ref Expression
1 nfimd.1 φ x ψ
2 nfimd.2 φ x χ
3 19.35 x ψ χ x ψ x χ
4 3 biimpi x ψ χ x ψ x χ
5 1 nfrd φ x ψ x ψ
6 2 nfrd φ x χ x χ
7 5 6 imim12d φ x ψ x χ x ψ x χ
8 19.38 x ψ x χ x ψ χ
9 4 7 8 syl56 φ x ψ χ x ψ χ
10 9 nfd φ x ψ χ