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

Theorem nfimd 1863
Description: If in a context 𝑥 is not free in 𝜓 and 𝜒, it is not free in (𝜓𝜒). Deduction form of nfimt 1861. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1750 changed. (Revised by Wolf Lammen, 18-Sep-2021.)
Hypotheses
Ref Expression
nfimd.1 (𝜑 → Ⅎ𝑥𝜓)
nfimd.2 (𝜑 → Ⅎ𝑥𝜒)
Assertion
Ref Expression
nfimd (𝜑 → Ⅎ𝑥(𝜓𝜒))

Proof of Theorem nfimd
StepHypRef Expression
1 nfimd.1 . 2 (𝜑 → Ⅎ𝑥𝜓)
2 nfimd.2 . 2 (𝜑 → Ⅎ𝑥𝜒)
3 nfimt2 1862 . 2 ((Ⅎ𝑥𝜓 ∧ Ⅎ𝑥𝜒) → Ⅎ𝑥(𝜓𝜒))
41, 2, 3syl2anc 694 1 (𝜑 → Ⅎ𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-nf 1750
This theorem is referenced by:  nfand  1866  nfbid  1872  nfim1  2105  hbimd  2164  dvelimhw  2209  dvelimf  2365  nfmod2  2511  nfrald  2973  nfifd  4147  nfixp  7969  axrepndlem1  9452  axrepndlem2  9453  axunndlem1  9455  axunnd  9456  axpowndlem2  9458  axpowndlem3  9459  axpowndlem4  9460  axregndlem2  9463  axregnd  9464  axinfndlem1  9465  axinfnd  9466  axacndlem4  9470  axacndlem5  9471  axacnd  9472  bj-dvelimdv  32959  wl-mo2df  33482  wl-mo2t  33487  riotasv2d  34561  nfintd  42745
  Copyright terms: Public domain W3C validator