Theorem nfimd 1921

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

Syntax hints:   → wi 4  ∀wal 1565  ∃wex 1806  Ⅎwnf 1810

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

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-nf 1811

This theorem is referenced by:  nfimt  1922  nfand  1924  nfbid  1929  nfim1  2241  hbimd  2339  dvelimhw  2383  dvelimf  2486  nfmod2  2592  nfmodv  2593  nfabdw  2952  nfraldw  3316  nfrald  3368  nfifd  4522  nfixpw  8916  nfixp  8917  axrepndlem1  10579  axrepndlem2  10580  axunndlem1  10582  axunnd  10583  axpowndlem2  10585  axpowndlem3  10586  axpowndlem4  10587  axregndlem2  10590  axregnd  10591  axinfndlem1  10592  axinfnd  10593  axacndlem4  10597  axacndlem5  10598  axacnd  10599  axpowg2  35495  axpowg3  35496  mh-setindnd  36973  bj-dvelimdv  37411  wl-mo2df  38150  wl-mo2t  38155  riotasv2d  39658  nfintd  50373