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

Theorem nf3an 1849
Description: If  x is not free in  ph,  ps, and  ch, it is not free in  ( ph  /\  ps  /\  ch ). (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypotheses
Ref Expression
nfan.1  |-  F/ x ph
nfan.2  |-  F/ x ps
nfan.3  |-  F/ x ch
Assertion
Ref Expression
nf3an  |-  F/ x
( ph  /\  ps  /\  ch )

Proof of Theorem nf3an
StepHypRef Expression
1 df-3an 938 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
2 nfan.1 . . . 4  |-  F/ x ph
3 nfan.2 . . . 4  |-  F/ x ps
42, 3nfan 1846 . . 3  |-  F/ x
( ph  /\  ps )
5 nfan.3 . . 3  |-  F/ x ch
64, 5nfan 1846 . 2  |-  F/ x
( ( ph  /\  ps )  /\  ch )
71, 6nfxfr 1579 1  |-  F/ x
( ph  /\  ps  /\  ch )
Colors of variables: wff set class
Syntax hints:    /\ wa 359    /\ w3a 936   F/wnf 1553
This theorem is referenced by:  hb3an  1852  vtocl3gaf  3012  mob  3108  reusv6OLD  4726  infpssrlem4  8178  axcc3  8310  axdc3lem4  8325  axdc4lem  8327  axacndlem4  8477  axacndlem5  8478  axacnd  8479  mreexexd  13865  iuncon  17483  hasheuni  24467  measvunilem  24558  measvunilem0  24559  measvuni  24560  volfiniune  24578  dedekind  25179  dedekindle  25180  nfcprod1  25228  nfcprod  25229  dfon2lem1  25402  dfon2lem3  25404  nfwrecs  25525  upixp  26422  sdclem1  26438  rfcnnnub  27674  fmuldfeqlem1  27679  fmuldfeq  27680  fmul01lt1  27683  infrglb  27689  stoweidlem16  27732  stoweidlem17  27733  stoweidlem19  27735  stoweidlem20  27736  stoweidlem22  27738  stoweidlem26  27742  stoweidlem28  27744  stoweidlem31  27747  stoweidlem34  27750  stoweidlem35  27751  stoweidlem48  27764  stoweidlem52  27768  stoweidlem53  27769  stoweidlem56  27772  stoweidlem57  27773  stoweidlem60  27776  tratrb  28557  bnj919  29073  bnj1379  29139  bnj571  29214  bnj607  29224  bnj873  29232  bnj964  29251  bnj981  29258  bnj1123  29292  bnj1128  29296  bnj1204  29318  bnj1279  29324  bnj1388  29339  bnj1398  29340  bnj1417  29347  bnj1444  29349  bnj1445  29350  bnj1449  29354  bnj1489  29362  bnj1518  29370  bnj1525  29375  pmapglbx  30503  cdlemefr29exN  31136
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-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator