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 848	. 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 847  Ⅎ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 848  df-ex 1780  df-nf 1784

This theorem is referenced by:  nf3or  1905  axi12  2705  axbnd  2706  nfun  4145  nfunOLD  4146  nfpr  4668  rabsnifsb  4698  disjxun  5117  fsuppmapnn0fiubex  14010  nfsum1  15706  nfsum  15707  nfcprod1  15924  nfcprod  15925  fdc1  37770  dvdsrabdioph  42833  mnringmulrcld  44252  disjinfi  45216  iundjiun  46489