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

Theorem nfor 1993
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 371 . 2  |-  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
2 nf.1 . . . 4  |-  F/ x ph
32nfn 1958 . . 3  |-  F/ x  -.  ph
4 nf.2 . . 3  |-  F/ x ps
53, 4nfim 1978 . 2  |-  F/ x
( -.  ph  ->  ps )
61, 5nfxfr 1692 1  |-  F/ x
( ph  \/  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 369   F/wnf 1663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-12 1907
This theorem depends on definitions:  df-bi 188  df-or 371  df-ex 1660  df-nf 1664
This theorem is referenced by:  nf3or  1994  axi12  2405  nfun  3628  nfpr  4050  rabsnifsb  4071  disjxun  4424  fsuppmapnn0fiubex  12201  nfsum1  13734  nfsum  13735  nfcprod1  13942  nfcprod  13943  fdc1  31779  dvdsrabdioph  35362  disjinfi  37091  iundjiun  37807
  Copyright terms: Public domain W3C validator