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

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
StepHypRef Expression
1 df-or 849 . 2 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
2 nf.1 . . . 4 𝑥𝜑
32nfn 1857 . . 3 𝑥 ¬ 𝜑
4 nf.2 . . 3 𝑥𝜓
53, 4nfim 1896 . 2 𝑥𝜑𝜓)
61, 5nfxfr 1853 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 848  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 849  df-ex 1780  df-nf 1784
This theorem is referenced by:  nf3or  1905  axi12  2706  axbnd  2707  nfun  4170  nfunOLD  4171  nfpr  4692  rabsnifsb  4722  disjxun  5141  fsuppmapnn0fiubex  14033  nfsum1  15726  nfsum  15727  nfcprod1  15944  nfcprod  15945  fdc1  37753  dvdsrabdioph  42821  mnringmulrcld  44247  disjinfi  45197  iundjiun  46475
  Copyright terms: Public domain W3C validator