Theorem nfor 1939

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 1931	. 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  1940  axi12  2733  axbnd  2734  nfun  4172  nfpr  4653  rabsnifsb  4683  disjxun  5104  fsuppmapnn0fiubex  14165  nfsum1  15889  nfsum  15890  nfcprod1  16109  nfcprod  16110  onprcf1of1ord  36068  fdc1  38883  dvdsrabdioph  44021  mnringmulrcld  45429  disjinfi  46422  iundjiun  47685