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

Theorem nfand 1863
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 1841 . . . 4  |-  ( ph  ->  F/ x  -.  ch )
52, 4nfimd 1855 . . 3  |-  ( ph  ->  F/ x ( ps 
->  -.  ch ) )
65nfnd 1841 . 2  |-  ( ph  ->  F/ x  -.  ( ps  ->  -.  ch )
)
71, 6nfxfrd 1617 1  |-  ( ph  ->  F/ x ( ps 
/\  ch ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591
This theorem is referenced by:  nf3and  1864  nfbid  1871  nfeld  2624  nfreud  2999  nfrmod  3000  nfrmo  3002  nfrab  3008  nfifd  3928  nfdisj  4385  dfid3  4748  nfriotad  6172  axrepndlem1  8870  axrepndlem2  8871  axunndlem1  8873  axunnd  8874  axregndlem2  8883  axinfndlem1  8886  axinfnd  8887  axacndlem4  8891  axacndlem5  8892  axacnd  8893  riotasv2d  32966
  Copyright terms: Public domain W3C validator