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

Theorem nfimd 1902
Description: If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓𝜒). Deduction form of nfim 1904. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1792 changed. (Revised by Wolf Lammen, 18-Sep-2021.) Eliminate curried form of nfimt 1903. (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 1885 . . . 4 (∃𝑥(𝜓𝜒) ↔ (∀𝑥𝜓 → ∃𝑥𝜒))
21biimpi 219 . . 3 (∃𝑥(𝜓𝜒) → (∀𝑥𝜓 → ∃𝑥𝜒))
3 nfimd.1 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfrd 1799 . . . 4 (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
5 nfimd.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜒)
65nfrd 1799 . . . 4 (𝜑 → (∃𝑥𝜒 → ∀𝑥𝜒))
74, 6imim12d 81 . . 3 (𝜑 → ((∀𝑥𝜓 → ∃𝑥𝜒) → (∃𝑥𝜓 → ∀𝑥𝜒)))
8 19.38 1846 . . 3 ((∃𝑥𝜓 → ∀𝑥𝜒) → ∀𝑥(𝜓𝜒))
92, 7, 8syl56 36 . 2 (𝜑 → (∃𝑥(𝜓𝜒) → ∀𝑥(𝜓𝜒)))
109nfd 1798 1 (𝜑 → Ⅎ𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1541  wex 1787  wnf 1791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817
This theorem depends on definitions:  df-bi 210  df-ex 1788  df-nf 1792
This theorem is referenced by:  nfimt  1903  nfand  1905  nfbid  1910  nfim1  2198  hbimd  2300  dvelimhw  2347  dvelimf  2448  nfmod2  2558  nfmodv  2559  nfabdw  2928  nfraldw  3145  nfraldwOLD  3146  nfrald  3147  nfifd  4483  nfixpw  8618  nfixp  8619  axrepndlem1  10231  axrepndlem2  10232  axunndlem1  10234  axunnd  10235  axpowndlem2  10237  axpowndlem3  10238  axpowndlem4  10239  axregndlem2  10242  axregnd  10243  axinfndlem1  10244  axinfnd  10245  axacndlem4  10249  axacndlem5  10250  axacnd  10251  bj-dvelimdv  34798  wl-mo2df  35489  wl-mo2t  35494  riotasv2d  36735  nfintd  46079
  Copyright terms: Public domain W3C validator