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

Theorem nfand 1872
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 371 . 2  |-  ( ( ps  /\  ch )  <->  -.  ( ps  ->  -.  ch ) )
2 nfand.1 . . . 4  |-  ( ph  ->  F/ x ps )
3 nfand.2 . . . . 5  |-  ( ph  ->  F/ x ch )
43nfnd 1850 . . . 4  |-  ( ph  ->  F/ x  -.  ch )
52, 4nfimd 1864 . . 3  |-  ( ph  ->  F/ x ( ps 
->  -.  ch ) )
65nfnd 1850 . 2  |-  ( ph  ->  F/ x  -.  ( ps  ->  -.  ch )
)
71, 6nfxfrd 1626 1  |-  ( ph  ->  F/ x ( ps 
/\  ch ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369   F/wnf 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600
This theorem is referenced by:  nf3and  1873  nfbid  1880  nfeld  2637  nfreud  3039  nfrmod  3040  nfrmo  3042  nfrab  3048  nfifd  3973  nfdisj  4435  dfid3  4802  nfriotad  6264  axrepndlem1  8979  axrepndlem2  8980  axunndlem1  8982  axunnd  8983  axregndlem2  8992  axinfndlem1  8995  axinfnd  8996  axacndlem4  9000  axacndlem5  9001  axacnd  9002  riotasv2d  34116
  Copyright terms: Public domain W3C validator