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

Theorem nfand 2008
Description: If in a context  x is not free in  ps and  ch, it is not free in  ( ps  /\  ch ). (Contributed by Mario Carneiro, 7-Oct-2016.)
Hypotheses
Ref Expression
nfand.1  |-  ( ph  ->  F/ x ps )
nfand.2  |-  ( ph  ->  F/ x ch )
Assertion
Ref Expression
nfand  |-  ( ph  ->  F/ x ( ps 
/\  ch ) )

Proof of Theorem nfand
StepHypRef Expression
1 df-an 373 . 2  |-  ( ( ps  /\  ch )  <->  -.  ( ps  ->  -.  ch ) )
2 nfand.1 . . . 4  |-  ( ph  ->  F/ x ps )
3 nfand.2 . . . . 5  |-  ( ph  ->  F/ x ch )
43nfnd 1984 . . . 4  |-  ( ph  ->  F/ x  -.  ch )
52, 4nfimd 2000 . . 3  |-  ( ph  ->  F/ x ( ps 
->  -.  ch ) )
65nfnd 1984 . 2  |-  ( ph  ->  F/ x  -.  ( ps  ->  -.  ch )
)
71, 6nfxfrd 1697 1  |-  ( ph  ->  F/ x ( ps 
/\  ch ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 371   F/wnf 1667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-12 1933
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668
This theorem is referenced by:  nf3and  2009  nfbid  2016  nfeld  2600  nfreud  2963  nfrmod  2964  nfrmo  2966  nfrab  2972  nfifd  3909  nfdisj  4385  dfid3  4750  nfriotad  6260  axrepndlem1  9017  axrepndlem2  9018  axunndlem1  9020  axunnd  9021  axregndlem2  9028  axinfndlem1  9030  axinfnd  9031  axacndlem4  9035  axacndlem5  9036  axacnd  9037  riotasv2d  32529
  Copyright terms: Public domain W3C validator