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

Theorem nfand 1763
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 1760 . . . 4  |-  ( ph  ->  F/ x  -.  ch )
52, 4nfimd 1761 . . 3  |-  ( ph  ->  F/ x ( ps 
->  -.  ch ) )
65nfnd 1760 . 2  |-  ( ph  ->  F/ x  -.  ( ps  ->  -.  ch )
)
71, 6nfxfrd 1558 1  |-  ( ph  ->  F/ x ( ps 
/\  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358   F/wnf 1531
This theorem is referenced by:  nf3and  1764  nfeld  2434  nfreud  2712  nfrmod  2713  nfrmo  2715  nfrab  2721  nfifd  3588  nfdisj  4005  dfid3  4310  nfriotad  6313  riotasv2d  6349  riotasv3dOLD  6354  axrepndlem1  8214  axrepndlem2  8215  axunndlem1  8217  axunnd  8218  axregndlem2  8225  axinfndlem1  8227  axinfnd  8228  axacndlem4  8232  axacndlem5  8233  axacnd  8234
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532
  Copyright terms: Public domain W3C validator