Theorem nfimd 1927

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

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

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

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  nfimt  1928  nfand  1930  nfbid  1935  nfim1  2237  hbimd  2333  dvelimhw  2376  dvelimf  2479  nfmod2  2585  nfmodv  2586  nfabdw  2945  nfraldw  3309  nfrald  3359  nfifd  4515  nfixpw  8926  nfixp  8927  axrepndlem1  10602  axrepndlem2  10603  axunndlem1  10605  axunnd  10606  axpowndlem2  10608  axpowndlem3  10609  axpowndlem4  10610  axregndlem2  10613  axregnd  10614  axinfndlem1  10615  axinfnd  10616  axacndlem4  10620  axacndlem5  10621  axacnd  10622  axpowg2  35658  axpowg3  35659  mh-setindnd  37141  bj-dvelimdv  37579  wl-mo2df  38318  wl-mo2t  38323  riotasv2d  39815  nfintd  50584