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

Theorem nfimd 1889
Description: If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓𝜒). Deduction form of nfim 1891. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1778 changed. (Revised by Wolf Lammen, 18-Sep-2021.) Eliminate curried form of nfimt 1890. (Revised by Wolf Lammen, 10-Jul-2022.)
Hypotheses
Ref Expression
nfimd.1 (𝜑 → Ⅎ𝑥𝜓)
nfimd.2 (𝜑 → Ⅎ𝑥𝜒)
Assertion
Ref Expression
nfimd (𝜑 → Ⅎ𝑥(𝜓𝜒))

Proof of Theorem nfimd
StepHypRef Expression
1 19.35 1872 . . . 4 (∃𝑥(𝜓𝜒) ↔ (∀𝑥𝜓 → ∃𝑥𝜒))
21biimpi 215 . . 3 (∃𝑥(𝜓𝜒) → (∀𝑥𝜓 → ∃𝑥𝜒))
3 nfimd.1 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfrd 1785 . . . 4 (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
5 nfimd.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜒)
65nfrd 1785 . . . 4 (𝜑 → (∃𝑥𝜒 → ∀𝑥𝜒))
74, 6imim12d 81 . . 3 (𝜑 → ((∀𝑥𝜓 → ∃𝑥𝜒) → (∃𝑥𝜓 → ∀𝑥𝜒)))
8 19.38 1833 . . 3 ((∃𝑥𝜓 → ∀𝑥𝜒) → ∀𝑥(𝜓𝜒))
92, 7, 8syl56 36 . 2 (𝜑 → (∃𝑥(𝜓𝜒) → ∀𝑥(𝜓𝜒)))
109nfd 1784 1 (𝜑 → Ⅎ𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1531  wex 1773  wnf 1777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 206  df-ex 1774  df-nf 1778
This theorem is referenced by:  nfimt  1890  nfand  1892  nfbid  1897  nfim1  2184  hbimd  2286  dvelimhw  2333  dvelimf  2439  nfmod2  2544  nfmodv  2545  nfabdw  2918  nfraldw  3298  nfraldwOLD  3310  nfrald  3360  nfifd  4550  nfixpw  8907  nfixp  8908  axrepndlem1  10584  axrepndlem2  10585  axunndlem1  10587  axunnd  10588  axpowndlem2  10590  axpowndlem3  10591  axpowndlem4  10592  axregndlem2  10595  axregnd  10596  axinfndlem1  10597  axinfnd  10598  axacndlem4  10602  axacndlem5  10603  axacnd  10604  bj-dvelimdv  36221  wl-mo2df  36929  wl-mo2t  36934  riotasv2d  38321  nfintd  47930
  Copyright terms: Public domain W3C validator