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

Theorem nfimd 1820
Description: If in a context 𝑥 is not free in 𝜓 and 𝜒, it is not free in (𝜓𝜒). Deduction form of nfimt 1818. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1707 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 1819 . 2 ((Ⅎ𝑥𝜓 ∧ Ⅎ𝑥𝜒) → Ⅎ𝑥(𝜓𝜒))
41, 2, 3syl2anc 692 1 (𝜑 → Ⅎ𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-nf 1707
This theorem is referenced by:  nfand  1823  nfbid  1829  nfim1  2065  hbimd  2122  dvelimhw  2170  dvelimf  2333  nfmod2  2482  nfrald  2939  nfifd  4086  nfixp  7871  axrepndlem1  9358  axrepndlem2  9359  axunndlem1  9361  axunnd  9362  axpowndlem2  9364  axpowndlem3  9365  axpowndlem4  9366  axregndlem2  9369  axregnd  9370  axinfndlem1  9371  axinfnd  9372  axacndlem4  9376  axacndlem5  9377  axacnd  9378  bj-dvelimdv  32476  wl-mo2df  32981  wl-mo2t  32986  riotasv2d  33720  nfintd  41709
  Copyright terms: Public domain W3C validator