Theorem nfimd 1896

Description: If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓 → 𝜒). Deduction form of nfim 1898. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1786 changed. (Revised by Wolf Lammen, 18-Sep-2021.) Eliminate curried form of nfimt 1897. (Revised by Wolf Lammen, 10-Jul-2022.)

Hypotheses

Ref	Expression
nfimd.1	⊢ (𝜑 → Ⅎ𝑥𝜓)
nfimd.2	⊢ (𝜑 → Ⅎ𝑥𝜒)

Assertion

Ref	Expression
nfimd	⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒))

Proof of Theorem nfimd

Step	Hyp	Ref	Expression
1		19.35 1879	. . . 4 ⊢ (∃𝑥(𝜓 → 𝜒) ↔ (∀𝑥𝜓 → ∃𝑥𝜒))
2	1	biimpi 216	. . 3 ⊢ (∃𝑥(𝜓 → 𝜒) → (∀𝑥𝜓 → ∃𝑥𝜒))
3		nfimd.1	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfrd 1793	. . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
5		nfimd.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒)
6	5	nfrd 1793	. . . 4 ⊢ (𝜑 → (∃𝑥𝜒 → ∀𝑥𝜒))
7	4, 6	imim12d 81	. . 3 ⊢ (𝜑 → ((∀𝑥𝜓 → ∃𝑥𝜒) → (∃𝑥𝜓 → ∀𝑥𝜒)))
8		19.38 1841	. . 3 ⊢ ((∃𝑥𝜓 → ∀𝑥𝜒) → ∀𝑥(𝜓 → 𝜒))
9	2, 7, 8	syl56 36	. 2 ⊢ (𝜑 → (∃𝑥(𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒)))
10	9	nfd 1792	1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒))

Syntax hints:   → wi 4  ∀wal 1540  ∃wex 1781  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfimt  1897  nfand  1899  nfbid  1904  nfim1  2207  hbimd  2305  dvelimhw  2350  dvelimf  2453  nfmod2  2559  nfmodv  2560  nfabdw  2921  nfraldw  3283  nfrald  3344  nfifd  4511  nfixpw  8866  nfixp  8867  axrepndlem1  10515  axrepndlem2  10516  axunndlem1  10518  axunnd  10519  axpowndlem2  10521  axpowndlem3  10522  axpowndlem4  10523  axregndlem2  10526  axregnd  10527  axinfndlem1  10528  axinfnd  10529  axacndlem4  10533  axacndlem5  10534  axacnd  10535  mh-setindnd  36693  bj-dvelimdv  37103  wl-mo2df  37829  wl-mo2t  37834  riotasv2d  39337  nfintd  50036