Theorem nfimd 1896

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

Syntax hints:   → wi 4  ∀wal 1540  ∃wex 1781  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfimt  1897  nfand  1899  nfbid  1904  nfim1  2207  hbimd  2305  dvelimhw  2350  dvelimf  2453  nfmod2  2559  nfmodv  2560  nfabdw  2921  nfraldw  3283  nfrald  3335  nfifd  4497  nfixpw  8859  nfixp  8860  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  mh-setindnd  36739  bj-dvelimdv  37178  wl-mo2df  37913  wl-mo2t  37918  riotasv2d  39421  nfintd  50164