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

Theorem nfimd 1892
Description: If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓𝜒). Deduction form of nfim 1894. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1781 changed. (Revised by Wolf Lammen, 18-Sep-2021.) Eliminate curried form of nfimt 1893. (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 1875 . . . 4 (∃𝑥(𝜓𝜒) ↔ (∀𝑥𝜓 → ∃𝑥𝜒))
21biimpi 216 . . 3 (∃𝑥(𝜓𝜒) → (∀𝑥𝜓 → ∃𝑥𝜒))
3 nfimd.1 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfrd 1788 . . . 4 (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
5 nfimd.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜒)
65nfrd 1788 . . . 4 (𝜑 → (∃𝑥𝜒 → ∀𝑥𝜒))
74, 6imim12d 81 . . 3 (𝜑 → ((∀𝑥𝜓 → ∃𝑥𝜒) → (∃𝑥𝜓 → ∀𝑥𝜒)))
8 19.38 1836 . . 3 ((∃𝑥𝜓 → ∀𝑥𝜒) → ∀𝑥(𝜓𝜒))
92, 7, 8syl56 36 . 2 (𝜑 → (∃𝑥(𝜓𝜒) → ∀𝑥(𝜓𝜒)))
109nfd 1787 1 (𝜑 → Ⅎ𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1535  wex 1776  wnf 1780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806
This theorem depends on definitions:  df-bi 207  df-ex 1777  df-nf 1781
This theorem is referenced by:  nfimt  1893  nfand  1895  nfbid  1900  nfim1  2197  hbimd  2297  dvelimhw  2346  dvelimf  2451  nfmod2  2556  nfmodv  2557  nfabdw  2925  nfraldw  3307  nfrald  3370  nfifd  4560  nfixpw  8955  nfixp  8956  axrepndlem1  10630  axrepndlem2  10631  axunndlem1  10633  axunnd  10634  axpowndlem2  10636  axpowndlem3  10637  axpowndlem4  10638  axregndlem2  10641  axregnd  10642  axinfndlem1  10643  axinfnd  10644  axacndlem4  10648  axacndlem5  10649  axacnd  10650  bj-dvelimdv  36834  wl-mo2df  37551  wl-mo2t  37556  riotasv2d  38939  nfintd  48904
  Copyright terms: Public domain W3C validator