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

Theorem nfand 1833
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 361 . 2  |-  ( ( ps  /\  ch )  <->  -.  ( ps  ->  -.  ch ) )
2 nfand.1 . . . 4  |-  ( ph  ->  F/ x ps )
3 nfand.2 . . . . 5  |-  ( ph  ->  F/ x ch )
43nfnd 1799 . . . 4  |-  ( ph  ->  F/ x  -.  ch )
52, 4nfimd 1817 . . 3  |-  ( ph  ->  F/ x ( ps 
->  -.  ch ) )
65nfnd 1799 . 2  |-  ( ph  ->  F/ x  -.  ( ps  ->  -.  ch )
)
71, 6nfxfrd 1577 1  |-  ( ph  ->  F/ x ( ps 
/\  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359   F/wnf 1550
This theorem is referenced by:  nf3and  1834  nfbid  1844  nfeld  2538  nfreud  2823  nfrmod  2824  nfrmo  2826  nfrab  2832  nfifd  3705  nfdisj  4135  dfid3  4440  nfriotad  6494  riotasv2d  6530  riotasv3dOLD  6535  axrepndlem1  8400  axrepndlem2  8401  axunndlem1  8403  axunnd  8404  axregndlem2  8411  axinfndlem1  8413  axinfnd  8414  axacndlem4  8418  axacndlem5  8419  axacnd  8420
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator