Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfor Structured version   Visualization version   GIF version

Theorem nfor 1874
 Description: If 𝑥 is not free in 𝜑 and 𝜓, 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
StepHypRef Expression
1 df-or 384 . 2 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
2 nf.1 . . . 4 𝑥𝜑
32nfn 1824 . . 3 𝑥 ¬ 𝜑
4 nf.2 . . 3 𝑥𝜓
53, 4nfim 1865 . 2 𝑥𝜑𝜓)
61, 5nfxfr 1819 1 𝑥(𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382  Ⅎwnf 1748 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750 This theorem is referenced by:  nf3or  1875  axi12  2629  nfun  3802  nfpr  4264  rabsnifsb  4289  disjxun  4683  fsuppmapnn0fiubex  12832  nfsum1  14464  nfsum  14465  nfcprod1  14684  nfcprod  14685  fdc1  33672  dvdsrabdioph  37691  disjinfi  39694  iundjiun  40995
 Copyright terms: Public domain W3C validator