Theorem nfimd 1902

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

Syntax hints:   → wi 4  ∀wal 1546  ∃wex 1787  Ⅎwnf 1791

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

This theorem depends on definitions:  df-bi 209  df-ex 1788  df-nf 1792

This theorem is referenced by:  nfimt  1903  nfand  1905  nfbid  1910  nfim1  2213  hbimd  2311  dvelimhw  2355  dvelimf  2458  nfmod2  2564  nfmodv  2565  nfabdw  2924  nfraldw  3286  nfrald  3338  nfifd  4487  nfixpw  8858  nfixp  8859  axrepndlem1  10510  axrepndlem2  10511  axunndlem1  10513  axunnd  10514  axpowndlem2  10516  axpowndlem3  10517  axpowndlem4  10518  axregndlem2  10521  axregnd  10522  axinfndlem1  10523  axinfnd  10524  axacndlem4  10528  axacndlem5  10529  axacnd  10530  axpowg2  35343  axpowg3  35344  mh-setindnd  36780  bj-dvelimdv  37219  wl-mo2df  37956  wl-mo2t  37961  riotasv2d  39464  nfintd  50177