Theorem nfimd 1998

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

Syntax hints:   → wi 4  ∀wal 1656  ∃wex 1880  Ⅎwnf 1884

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

This theorem depends on definitions:  df-bi 199  df-ex 1881  df-nf 1885

This theorem is referenced by:  nfimt  1999  nfand  2002  nfbid  2007  nfim1  2241  hbimd  2332  dvelimhw  2371  dvelimf  2469  nfmod2  2627  nfmodv  2628  nfmod2OLD  2677  nfrald  3153  nfifd  4334  nfixp  8194  axrepndlem1  9729  axrepndlem2  9730  axunndlem1  9732  axunnd  9733  axpowndlem2  9735  axpowndlem3  9736  axpowndlem4  9737  axregndlem2  9740  axregnd  9741  axinfndlem1  9742  axinfnd  9743  axacndlem4  9747  axacndlem5  9748  axacnd  9749  bj-dvelimdv  33357  wl-mo2df  33896  wl-mo2t  33901  riotasv2d  35032  nfintd  43315