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

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

Proof of Theorem nfand
StepHypRef Expression
1 df-an 360 . 2  |-  ( ( ps  /\  ch )  <->  -.  ( ps  ->  -.  ch ) )
2 nfnd.1 . . . 4  |-  ( ph  ->  F/ x ps )
3 nfimd.2 . . . . 5  |-  ( ph  ->  F/ x ch )
43nfnd 1772 . . . 4  |-  ( ph  ->  F/ x  -.  ch )
52, 4nfimd 1773 . . 3  |-  ( ph  ->  F/ x ( ps 
->  -.  ch ) )
65nfnd 1772 . 2  |-  ( ph  ->  F/ x  -.  ( ps  ->  -.  ch )
)
71, 6nfxfrd 1561 1  |-  ( ph  ->  F/ x ( ps 
/\  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358   F/wnf 1534
This theorem is referenced by:  nf3and  1776  nfeld  2447  nfreud  2725  nfrmod  2726  nfrmo  2728  nfrab  2734  nfifd  3601  nfdisj  4021  dfid3  4326  nfriotad  6329  riotasv2d  6365  riotasv3dOLD  6370  axrepndlem1  8230  axrepndlem2  8231  axunndlem1  8233  axunnd  8234  axregndlem2  8241  axinfndlem1  8243  axinfnd  8244  axacndlem4  8248  axacndlem5  8249  axacnd  8250
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1535
  Copyright terms: Public domain W3C validator