Theorem nfor 1904

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 849	. 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
2		nf.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1857	. . 3 ⊢ Ⅎ𝑥 ¬ 𝜑
4		nf.2	. . 3 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1896	. 2 ⊢ Ⅎ𝑥(¬ 𝜑 → 𝜓)
6	1, 5	nfxfr 1853	1 ⊢ Ⅎ𝑥(𝜑 ∨ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 848  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784

This theorem is referenced by:  nf3or  1905  axi12  2706  axbnd  2707  nfun  4170  nfunOLD  4171  nfpr  4692  rabsnifsb  4722  disjxun  5141  fsuppmapnn0fiubex  14033  nfsum1  15726  nfsum  15727  nfcprod1  15944  nfcprod  15945  fdc1  37753  dvdsrabdioph  42821  mnringmulrcld  44247  disjinfi  45197  iundjiun  46475