Theorem nfimd 1812

Description: If in a context 𝑥 is not free in 𝜓 and 𝜒, it is not free in (𝜓 → 𝜒). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1701 changed. (Revised by Wolf Lammen, 18-Sep-2021.)

Hypotheses

Ref	Expression
nfimd.1	⊢ (𝜑 → Ⅎ𝑥𝜓)
nfimd.2	⊢ (𝜑 → Ⅎ𝑥𝜒)

Assertion

Ref	Expression
nfimd	⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒))

Proof of Theorem nfimd

Step	Hyp	Ref	Expression
1		19.35 1794	. . 3 ⊢ (∃𝑥(𝜓 → 𝜒) ↔ (∀𝑥𝜓 → ∃𝑥𝜒))
2		nfimd.1	. . . . . 6 ⊢ (𝜑 → Ⅎ𝑥𝜓)
3		nf4 1704	. . . . . 6 ⊢ (Ⅎ𝑥𝜓 ↔ (¬ ∀𝑥𝜓 → ∀𝑥 ¬ 𝜓))
4	2, 3	sylib 207	. . . . 5 ⊢ (𝜑 → (¬ ∀𝑥𝜓 → ∀𝑥 ¬ 𝜓))
5		pm2.21 119	. . . . . 6 ⊢ (¬ 𝜓 → (𝜓 → 𝜒))
6	5	alimi 1730	. . . . 5 ⊢ (∀𝑥 ¬ 𝜓 → ∀𝑥(𝜓 → 𝜒))
7	4, 6	syl6 34	. . . 4 ⊢ (𝜑 → (¬ ∀𝑥𝜓 → ∀𝑥(𝜓 → 𝜒)))
8		nfimd.2	. . . . . 6 ⊢ (𝜑 → Ⅎ𝑥𝜒)
9	8	nfrd 1708	. . . . 5 ⊢ (𝜑 → (∃𝑥𝜒 → ∀𝑥𝜒))
10		ala1 1755	. . . . 5 ⊢ (∀𝑥𝜒 → ∀𝑥(𝜓 → 𝜒))
11	9, 10	syl6 34	. . . 4 ⊢ (𝜑 → (∃𝑥𝜒 → ∀𝑥(𝜓 → 𝜒)))
12	7, 11	jad 173	. . 3 ⊢ (𝜑 → ((∀𝑥𝜓 → ∃𝑥𝜒) → ∀𝑥(𝜓 → 𝜒)))
13	1, 12	syl5bi 231	. 2 ⊢ (𝜑 → (∃𝑥(𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒)))
14	13	nfd 1707	1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒))

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1473  ∃wex 1695  Ⅎwnf 1699

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

This theorem depends on definitions:  df-bi 196  df-or 384  df-ex 1696  df-nf 1701

This theorem is referenced by:  nfim  1813  nfand  1814  nfbid  1820  nfim1  2055  hbimd  2111  dvelimhw  2159  dvelimf  2322  nfmod2  2471  nfrald  2928  nfifd  4064  nfixp  7813  axrepndlem1  9293  axrepndlem2  9294  axunndlem1  9296  axunnd  9297  axpowndlem2  9299  axpowndlem3  9300  axpowndlem4  9301  axregndlem2  9304  axregnd  9305  axinfndlem1  9306  axinfnd  9307  axacndlem4  9311  axacndlem5  9312  axacnd  9313  bj-dvelimdv  32027  wl-mo2df  32531  wl-mo2t  32536  riotasv2d  33261  nfintd  42218