Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfimd Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 19.35 1794 . . 3 (∃𝑥(𝜓𝜒) ↔ (∀𝑥𝜓 → ∃𝑥𝜒))
2 nfimd.1 . . . . . 6 (𝜑 → Ⅎ𝑥𝜓)
3 nf4 1704 . . . . . 6 (Ⅎ𝑥𝜓 ↔ (¬ ∀𝑥𝜓 → ∀𝑥 ¬ 𝜓))
42, 3sylib 207 . . . . 5 (𝜑 → (¬ ∀𝑥𝜓 → ∀𝑥 ¬ 𝜓))
5 pm2.21 119 . . . . . 6 𝜓 → (𝜓𝜒))
65alimi 1730 . . . . 5 (∀𝑥 ¬ 𝜓 → ∀𝑥(𝜓𝜒))
74, 6syl6 34 . . . 4 (𝜑 → (¬ ∀𝑥𝜓 → ∀𝑥(𝜓𝜒)))
8 nfimd.2 . . . . . 6 (𝜑 → Ⅎ𝑥𝜒)
98nfrd 1708 . . . . 5 (𝜑 → (∃𝑥𝜒 → ∀𝑥𝜒))
10 ala1 1755 . . . . 5 (∀𝑥𝜒 → ∀𝑥(𝜓𝜒))
119, 10syl6 34 . . . 4 (𝜑 → (∃𝑥𝜒 → ∀𝑥(𝜓𝜒)))
127, 11jad 173 . . 3 (𝜑 → ((∀𝑥𝜓 → ∃𝑥𝜒) → ∀𝑥(𝜓𝜒)))
131, 12syl5bi 231 . 2 (𝜑 → (∃𝑥(𝜓𝜒) → ∀𝑥(𝜓𝜒)))
1413nfd 1707 1 (𝜑 → Ⅎ𝑥(𝜓𝜒))
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator