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

Theorem nfimd 1893
Description: If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓𝜒). Deduction form of nfim 1895. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1783 changed. (Revised by Wolf Lammen, 18-Sep-2021.) Eliminate curried form of nfimt 1894. (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 1876 . . . 4 (∃𝑥(𝜓𝜒) ↔ (∀𝑥𝜓 → ∃𝑥𝜒))
21biimpi 216 . . 3 (∃𝑥(𝜓𝜒) → (∀𝑥𝜓 → ∃𝑥𝜒))
3 nfimd.1 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfrd 1790 . . . 4 (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
5 nfimd.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜒)
65nfrd 1790 . . . 4 (𝜑 → (∃𝑥𝜒 → ∀𝑥𝜒))
74, 6imim12d 81 . . 3 (𝜑 → ((∀𝑥𝜓 → ∃𝑥𝜒) → (∃𝑥𝜓 → ∀𝑥𝜒)))
8 19.38 1838 . . 3 ((∃𝑥𝜓 → ∀𝑥𝜒) → ∀𝑥(𝜓𝜒))
92, 7, 8syl56 36 . 2 (𝜑 → (∃𝑥(𝜓𝜒) → ∀𝑥(𝜓𝜒)))
109nfd 1789 1 (𝜑 → Ⅎ𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1537  wex 1778  wnf 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808
This theorem depends on definitions:  df-bi 207  df-ex 1779  df-nf 1783
This theorem is referenced by:  nfimt  1894  nfand  1896  nfbid  1901  nfim1  2198  hbimd  2297  dvelimhw  2346  dvelimf  2452  nfmod2  2557  nfmodv  2558  nfabdw  2926  nfraldw  3308  nfrald  3371  nfifd  4554  nfixpw  8957  nfixp  8958  axrepndlem1  10633  axrepndlem2  10634  axunndlem1  10636  axunnd  10637  axpowndlem2  10639  axpowndlem3  10640  axpowndlem4  10641  axregndlem2  10644  axregnd  10645  axinfndlem1  10646  axinfnd  10647  axacndlem4  10651  axacndlem5  10652  axacnd  10653  bj-dvelimdv  36853  wl-mo2df  37572  wl-mo2t  37577  riotasv2d  38959  nfintd  49247
  Copyright terms: Public domain W3C validator