Theorem nfimd 1897

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

Syntax hints:   → wi 4  ∀wal 1537  ∃wex 1782  Ⅎwnf 1786

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

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfimt  1898  nfand  1900  nfbid  1905  nfim1  2192  hbimd  2295  dvelimhw  2343  dvelimf  2448  nfmod2  2558  nfmodv  2559  nfabdw  2930  nfraldw  3148  nfraldwOLD  3149  nfrald  3150  nfifd  4488  nfixpw  8704  nfixp  8705  axrepndlem1  10348  axrepndlem2  10349  axunndlem1  10351  axunnd  10352  axpowndlem2  10354  axpowndlem3  10355  axpowndlem4  10356  axregndlem2  10359  axregnd  10360  axinfndlem1  10361  axinfnd  10362  axacndlem4  10366  axacndlem5  10367  axacnd  10368  bj-dvelimdv  35035  wl-mo2df  35725  wl-mo2t  35730  riotasv2d  36971  nfintd  46379