Theorem nfimd 1924

Description: If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓 → 𝜒). Deduction form of nfim 1926. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1814 changed. (Revised by Wolf Lammen, 18-Sep-2021.) Eliminate curried form of nfimt 1925. (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 1907	. . . 4 ⊢ (∃𝑥(𝜓 → 𝜒) ↔ (∀𝑥𝜓 → ∃𝑥𝜒))
2	1	biimpi 219	. . 3 ⊢ (∃𝑥(𝜓 → 𝜒) → (∀𝑥𝜓 → ∃𝑥𝜒))
3		nfimd.1	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfrd 1821	. . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
5		nfimd.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒)
6	5	nfrd 1821	. . . 4 ⊢ (𝜑 → (∃𝑥𝜒 → ∀𝑥𝜒))
7	4, 6	imim12d 82	. . 3 ⊢ (𝜑 → ((∀𝑥𝜓 → ∃𝑥𝜒) → (∃𝑥𝜓 → ∀𝑥𝜒)))
8		19.38 1869	. . 3 ⊢ ((∃𝑥𝜓 → ∀𝑥𝜒) → ∀𝑥(𝜓 → 𝜒))
9	2, 7, 8	syl56 37	. 2 ⊢ (𝜑 → (∃𝑥(𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒)))
10	9	nfd 1820	1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒))

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  ∃wex 1809  Ⅎwnf 1813

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839

This proof depends on definitions:  df-bi 210  df-ex 1810  df-nf 1814

This theorem is used by:  nfimt  1925  nfand  1927  nfbid  1932  nfim1  2235  hbimd  2333  dvelimhw  2377  dvelimf  2480  nfmod2  2586  nfmodv  2587  nfabdw  2946  nfraldw  3310  nfrald  3361  nfifd  4517  nfixpw  8910  nfixp  8911  axrepndlem1  10581  axrepndlem2  10582  axunndlem1  10584  axunnd  10585  axpowndlem2  10587  axpowndlem3  10588  axpowndlem4  10589  axregndlem2  10592  axregnd  10593  axinfndlem1  10594  axinfnd  10595  axacndlem4  10599  axacndlem5  10600  axacnd  10601  axpowg2  35568  axpowg3  35569  mh-setindnd  37076  bj-dvelimdv  37514  wl-mo2df  38253  wl-mo2t  38258  riotasv2d  39759  nfintd  50479