MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfrd Unicode version

Theorem nfrd 1875
Description: Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfrd.1
Assertion
Ref Expression
nfrd

Proof of Theorem nfrd
StepHypRef Expression
1 nfrd.1 . 2
2 nfr 1873 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1393  F/wnf 1616
This theorem is referenced by:  alrimdd  1880  nfdi  1916  nfim1  1919  hbimd  1921  nfan1  1927  nfald  1951  dvelimhw  1955  spimed  2007  cbv2  2020  dveeq2  2042  dveeq1  2044  axc9  2046  dvelimh  2078  abidnf  3268  eusvnfb  4648  axrepnd  8990  axacndlem4  9009  wl-nfeqfb  29990  bj-spimedv  34280  bj-cbv2v  34295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617
  Copyright terms: Public domain W3C validator