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

Theorem nfor 1902
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
StepHypRef Expression
1 df-or 848 . 2 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
2 nf.1 . . . 4 𝑥𝜑
32nfn 1855 . . 3 𝑥 ¬ 𝜑
4 nf.2 . . 3 𝑥𝜓
53, 4nfim 1894 . 2 𝑥𝜑𝜓)
61, 5nfxfr 1850 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 847  wnf 1780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-nf 1781
This theorem is referenced by:  nf3or  1903  axi12  2704  axbnd  2705  nfun  4180  nfunOLD  4181  nfpr  4697  rabsnifsb  4727  disjxun  5146  fsuppmapnn0fiubex  14030  nfsum1  15723  nfsum  15724  nfcprod1  15941  nfcprod  15942  fdc1  37733  dvdsrabdioph  42798  mnringmulrcld  44224  disjinfi  45135  iundjiun  46416
  Copyright terms: Public domain W3C validator