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

Theorem nfor 1831
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 385 . 2 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
2 nf.1 . . . 4 𝑥𝜑
32nfn 1781 . . 3 𝑥 ¬ 𝜑
4 nf.2 . . 3 𝑥𝜓
53, 4nfim 1822 . 2 𝑥𝜑𝜓)
61, 5nfxfr 1776 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 383  wnf 1705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707
This theorem is referenced by:  nf3or  1832  axi12  2599  nfun  3747  nfpr  4203  rabsnifsb  4227  disjxun  4611  fsuppmapnn0fiubex  12732  nfsum1  14354  nfsum  14355  nfcprod1  14565  nfcprod  14566  fdc1  33174  dvdsrabdioph  36854  disjinfi  38854  iundjiun  39984
  Copyright terms: Public domain W3C validator