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

Theorem nfor 2029
Description: If  x is not free in  ph and  ps, it is not free in  ( ph  \/  ps ). (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 11-Aug-2016.)
Hypotheses
Ref Expression
nf.1  |-  F/ x ph
nf.2  |-  F/ x ps
Assertion
Ref Expression
nfor  |-  F/ x
( ph  \/  ps )

Proof of Theorem nfor
StepHypRef Expression
1 df-or 376 . 2  |-  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
2 nf.1 . . . 4  |-  F/ x ph
32nfn 1994 . . 3  |-  F/ x  -.  ph
4 nf.2 . . 3  |-  F/ x ps
53, 4nfim 2014 . 2  |-  F/ x
( -.  ph  ->  ps )
61, 5nfxfr 1707 1  |-  F/ x
( ph  \/  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 374   F/wnf 1678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-12 1944
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-ex 1675  df-nf 1679
This theorem is referenced by:  nf3or  2030  axi12  2440  nfun  3602  nfpr  4031  rabsnifsb  4053  disjxun  4414  fsuppmapnn0fiubex  12236  nfsum1  13805  nfsum  13806  nfcprod1  14013  nfcprod  14014  fdc1  32120  dvdsrabdioph  35698  disjinfi  37506  iundjiun  38336
  Copyright terms: Public domain W3C validator