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

Theorem nfand 1843
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 1809 . . . 4  |-  ( ph  ->  F/ x  -.  ch )
52, 4nfimd 1827 . . 3  |-  ( ph  ->  F/ x ( ps 
->  -.  ch ) )
65nfnd 1809 . 2  |-  ( ph  ->  F/ x  -.  ( ps  ->  -.  ch )
)
71, 6nfxfrd 1580 1  |-  ( ph  ->  F/ x ( ps 
/\  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359   F/wnf 1553
This theorem is referenced by:  nf3and  1844  nfbid  1854  nfeld  2586  nfreud  2872  nfrmod  2873  nfrmo  2875  nfrab  2881  nfifd  3754  nfdisj  4186  dfid3  4491  nfriotad  6550  riotasv2d  6586  riotasv3dOLD  6591  axrepndlem1  8459  axrepndlem2  8460  axunndlem1  8462  axunnd  8463  axregndlem2  8470  axinfndlem1  8472  axinfnd  8473  axacndlem4  8477  axacndlem5  8478  axacnd  8479
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator