Theorem nfor 1868

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 835	. 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
2		nf.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1820	. . 3 ⊢ Ⅎ𝑥 ¬ 𝜑
4		nf.2	. . 3 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1860	. 2 ⊢ Ⅎ𝑥(¬ 𝜑 → 𝜓)
6	1, 5	nfxfr 1816	1 ⊢ Ⅎ𝑥(𝜑 ∨ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 834  Ⅎwnf 1747

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

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-ex 1744  df-nf 1748

This theorem is referenced by:  nf3or  1869  axi12  2739  axi12OLD  2740  axbnd  2741  nfun  4023  nfpr  4498  rabsnifsb  4528  disjxun  4923  fsuppmapnn0fiubex  13173  nfsum1  14905  nfsum  14906  nfcprod1  15122  nfcprod  15123  fdc1  34500  dvdsrabdioph  38841  disjinfi  40913  iundjiun  42207