Theorem nfor 1937

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 1890	. . 3 ⊢ Ⅎ𝑥 ¬ 𝜑
4		nf.2	. . 3 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1929	. 2 ⊢ Ⅎ𝑥(¬ 𝜑 → 𝜓)
6	1, 5	nfxfr 1886	1 ⊢ Ⅎ𝑥(𝜑 ∨ 𝜓)

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

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

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

This theorem is used by:  nf3or  1938  axi12  2732  axbnd  2733  nfun  4120  nfpr  4656  rabsnifsb  4686  disjxun  5105  fsuppmapnn0fiubex  14060  nfsum1  15781  nfsum  15782  nfcprod1  16001  nfcprod  16002  fdc1  38504  dvdsrabdioph  43659  mnringmulrcld  45074  disjinfi  46032  iundjiun  47296