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

Step	Hyp	Ref	Expression
1		nfrd.1	. 2
2		nfr 1873	. 2
3	1, 2	syl 16	1

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