Theorem nfor 1936

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 862	. 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
2		nf.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1889	. . 3 ⊢ Ⅎ𝑥 ¬ 𝜑
4		nf.2	. . 3 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1928	. 2 ⊢ Ⅎ𝑥(¬ 𝜑 → 𝜓)
6	1, 5	nfxfr 1885	1 ⊢ Ⅎ𝑥(𝜑 ∨ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 861  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-nf 1816

This theorem is used by:  nf3or  1937  axi12  2730  axbnd  2731  nfun  4169  nfpr  4649  rabsnifsb  4679  disjxun  5100  fsuppmapnn0fiubex  14139  nfsum1  15863  nfsum  15864  nfcprod1  16083  nfcprod  16084  onprcf1of1ord  35975  fdc1  38774  dvdsrabdioph  43911  mnringmulrcld  45320  disjinfi  46301  iundjiun  47564