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