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

Theorem nfor 1983
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 1933 . . 3 𝑥 ¬ 𝜑
4 nf.2 . . 3 𝑥𝜓
53, 4nfim 1974 . 2 𝑥𝜑𝜓)
61, 5nfxfr 1928 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 382  wnf 1857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1854  df-nf 1859
This theorem is referenced by:  nf3or  1984  axi12  2738  nfun  3912  nfpr  4376  rabsnifsb  4401  disjxun  4802  fsuppmapnn0fiubex  13006  nfsum1  14639  nfsum  14640  nfcprod1  14859  nfcprod  14860  fdc1  33873  dvdsrabdioph  37894  disjinfi  39897  iundjiun  41198
  Copyright terms: Public domain W3C validator