Theorem nfimd 1894

Description: If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓 → 𝜒). Deduction form of nfim 1896. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1784 changed. (Revised by Wolf Lammen, 18-Sep-2021.) Eliminate curried form of nfimt 1895. (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 1877	. . . 4 ⊢ (∃𝑥(𝜓 → 𝜒) ↔ (∀𝑥𝜓 → ∃𝑥𝜒))
2	1	biimpi 216	. . 3 ⊢ (∃𝑥(𝜓 → 𝜒) → (∀𝑥𝜓 → ∃𝑥𝜒))
3		nfimd.1	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfrd 1791	. . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
5		nfimd.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒)
6	5	nfrd 1791	. . . 4 ⊢ (𝜑 → (∃𝑥𝜒 → ∀𝑥𝜒))
7	4, 6	imim12d 81	. . 3 ⊢ (𝜑 → ((∀𝑥𝜓 → ∃𝑥𝜒) → (∃𝑥𝜓 → ∀𝑥𝜒)))
8		19.38 1839	. . 3 ⊢ ((∃𝑥𝜓 → ∀𝑥𝜒) → ∀𝑥(𝜓 → 𝜒))
9	2, 7, 8	syl56 36	. 2 ⊢ (𝜑 → (∃𝑥(𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒)))
10	9	nfd 1790	1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒))

Syntax hints:   → wi 4  ∀wal 1538  ∃wex 1779  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfimt  1895  nfand  1897  nfbid  1902  nfim1  2200  hbimd  2298  dvelimhw  2343  dvelimf  2446  nfmod2  2551  nfmodv  2552  nfabdw  2913  nfraldw  3274  nfrald  3335  nfifd  4506  nfixpw  8843  nfixp  8844  axrepndlem1  10486  axrepndlem2  10487  axunndlem1  10489  axunnd  10490  axpowndlem2  10492  axpowndlem3  10493  axpowndlem4  10494  axregndlem2  10497  axregnd  10498  axinfndlem1  10499  axinfnd  10500  axacndlem4  10504  axacndlem5  10505  axacnd  10506  bj-dvelimdv  36835  wl-mo2df  37554  wl-mo2t  37559  riotasv2d  38946  nfintd  49668