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  2235  hbimd  2331  dvelimhw  2374  dvelimf  2477  nfmod2  2583  nfmodv  2584  nfabdw  2943  nfraldw  3307  nfrald  3357  nfifd  4512  nfixpw  8930  nfixp  8931  axrepndlem1  10626  axrepndlem2  10627  axunndlem1  10629  axunnd  10630  axpowndlem2  10632  axpowndlem3  10633  axpowndlem4  10634  axregndlem2  10637  axregnd  10638  axinfndlem1  10639  axinfnd  10640  axacndlem4  10644  axacndlem5  10645  axacnd  10646  axpowg2  35716  axpowg3  35717  mh-setindnd  37223  bj-dvelimdv  37661  wl-mo2df  38398  wl-mo2t  38403  riotasv2d  39895  nfintd  50664