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

Theorem nfand 1930
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 369 . 2  |-  ( ( ps  /\  ch )  <->  -.  ( ps  ->  -.  ch ) )
2 nfand.1 . . . 4  |-  ( ph  ->  F/ x ps )
3 nfand.2 . . . . 5  |-  ( ph  ->  F/ x ch )
43nfnd 1907 . . . 4  |-  ( ph  ->  F/ x  -.  ch )
52, 4nfimd 1922 . . 3  |-  ( ph  ->  F/ x ( ps 
->  -.  ch ) )
65nfnd 1907 . 2  |-  ( ph  ->  F/ x  -.  ( ps  ->  -.  ch )
)
71, 6nfxfrd 1651 1  |-  ( ph  ->  F/ x ( ps 
/\  ch ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 367   F/wnf 1621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-nf 1622
This theorem is referenced by:  nf3and  1931  nfbid  1938  nfeld  2624  nfreud  3027  nfrmod  3028  nfrmo  3030  nfrab  3036  nfifd  3957  nfdisj  4422  dfid3  4785  nfriotad  6240  axrepndlem1  8958  axrepndlem2  8959  axunndlem1  8961  axunnd  8962  axregndlem2  8969  axinfndlem1  8972  axinfnd  8973  axacndlem4  8977  axacndlem5  8978  axacnd  8979  riotasv2d  35085
  Copyright terms: Public domain W3C validator