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

Theorem nfimd 1891
 Description: If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓 → 𝜒). Deduction form of nfim 1893. (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 1892. (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 1874 . . . 4 (∃𝑥(𝜓𝜒) ↔ (∀𝑥𝜓 → ∃𝑥𝜒))
21biimpi 218 . . 3 (∃𝑥(𝜓𝜒) → (∀𝑥𝜓 → ∃𝑥𝜒))
3 nfimd.1 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfrd 1788 . . . 4 (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
5 nfimd.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜒)
65nfrd 1788 . . . 4 (𝜑 → (∃𝑥𝜒 → ∀𝑥𝜒))
74, 6imim12d 81 . . 3 (𝜑 → ((∀𝑥𝜓 → ∃𝑥𝜒) → (∃𝑥𝜓 → ∀𝑥𝜒)))
8 19.38 1835 . . 3 ((∃𝑥𝜓 → ∀𝑥𝜒) → ∀𝑥(𝜓𝜒))
92, 7, 8syl56 36 . 2 (𝜑 → (∃𝑥(𝜓𝜒) → ∀𝑥(𝜓𝜒)))
109nfd 1787 1 (𝜑 → Ⅎ𝑥(𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1531  ∃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 209  df-ex 1777  df-nf 1781 This theorem is referenced by:  nfimt  1892  nfand  1894  nfbid  1899  nfim1  2194  hbimd  2302  dvelimhw  2362  dvelimf  2466  nfmod2  2638  nfmodv  2639  nfraldw  3223  nfrald  3224  nfifd  4495  nfixpw  8474  nfixp  8475  axrepndlem1  10008  axrepndlem2  10009  axunndlem1  10011  axunnd  10012  axpowndlem2  10014  axpowndlem3  10015  axpowndlem4  10016  axregndlem2  10019  axregnd  10020  axinfndlem1  10021  axinfnd  10022  axacndlem4  10026  axacndlem5  10027  axacnd  10028  bj-dvelimdv  34170  wl-mo2df  34800  wl-mo2t  34805  riotasv2d  36087  nfintd  44769
 Copyright terms: Public domain W3C validator