Theorem nfor 1907

Description: If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑 ∨ 𝜓). (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 11-Aug-2016.)

Hypotheses

Ref	Expression
nf.1	⊢ Ⅎ𝑥𝜑
nf.2	⊢ Ⅎ𝑥𝜓

Assertion

Ref	Expression
nfor	⊢ Ⅎ𝑥(𝜑 ∨ 𝜓)

Proof of Theorem nfor

Step	Hyp	Ref	Expression
1		df-or 846	. 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
2		nf.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1860	. . 3 ⊢ Ⅎ𝑥 ¬ 𝜑
4		nf.2	. . 3 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1899	. 2 ⊢ Ⅎ𝑥(¬ 𝜑 → 𝜓)
6	1, 5	nfxfr 1855	1 ⊢ Ⅎ𝑥(𝜑 ∨ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 845  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-nf 1786

This theorem is referenced by:  nf3or  1908  axi12  2700  axbnd  2701  nfun  4130  nfpr  4656  rabsnifsb  4688  disjxun  5108  fsuppmapnn0fiubex  13907  nfsum1  15586  nfsum  15587  nfcprod1  15804  nfcprod  15805  fdc1  36278  dvdsrabdioph  41191  mnringmulrcld  42630  disjinfi  43534  iundjiun  44821