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

Theorem nfimd 1998
Description: If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓𝜒). Deduction form of nfim 2001. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1885 changed. (Revised by Wolf Lammen, 18-Sep-2021.) Eliminate curried form of nfimt 1999. (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 1982 . . . 4 (∃𝑥(𝜓𝜒) ↔ (∀𝑥𝜓 → ∃𝑥𝜒))
21biimpi 208 . . 3 (∃𝑥(𝜓𝜒) → (∀𝑥𝜓 → ∃𝑥𝜒))
3 nfimd.1 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfrd 1892 . . . 4 (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
5 nfimd.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜒)
65nfrd 1892 . . . 4 (𝜑 → (∃𝑥𝜒 → ∀𝑥𝜒))
74, 6imim12d 81 . . 3 (𝜑 → ((∀𝑥𝜓 → ∃𝑥𝜒) → (∃𝑥𝜓 → ∀𝑥𝜒)))
8 19.38 1939 . . 3 ((∃𝑥𝜓 → ∀𝑥𝜒) → ∀𝑥(𝜓𝜒))
92, 7, 8syl56 36 . 2 (𝜑 → (∃𝑥(𝜓𝜒) → ∀𝑥(𝜓𝜒)))
109nfd 1891 1 (𝜑 → Ⅎ𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1656  wex 1880  wnf 1884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910
This theorem depends on definitions:  df-bi 199  df-ex 1881  df-nf 1885
This theorem is referenced by:  nfimt  1999  nfand  2002  nfbid  2007  nfim1  2241  hbimd  2332  dvelimhw  2371  dvelimf  2469  nfmod2  2627  nfmodv  2628  nfmod2OLD  2677  nfrald  3153  nfifd  4334  nfixp  8194  axrepndlem1  9729  axrepndlem2  9730  axunndlem1  9732  axunnd  9733  axpowndlem2  9735  axpowndlem3  9736  axpowndlem4  9737  axregndlem2  9740  axregnd  9741  axinfndlem1  9742  axinfnd  9743  axacndlem4  9747  axacndlem5  9748  axacnd  9749  bj-dvelimdv  33357  wl-mo2df  33896  wl-mo2t  33901  riotasv2d  35032  nfintd  43315
  Copyright terms: Public domain W3C validator