Theorem nf3an 1916

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

Step	Hyp	Ref	Expression
1		df-3an 976	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		nfan.1	. . . 4 |- F/ x ph
3		nfan.2	. . . 4 |- F/ x ps
4	2, 3	nfan 1914	. . 3 |- F/ x ( ph /\ ps )
5		nfan.3	. . 3 |- F/ x ch
6	4, 5	nfan 1914	. 2 |- F/ x ( ( ph /\ ps ) /\ ch )
7	1, 6	nfxfr 1632	1 |- F/ x ( ph /\ ps /\ ch )

Syntax hints:   /\ wa 369   /\ w3a 974   F/wnf 1603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-12 1840

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 976  df-ex 1600  df-nf 1604

This theorem is referenced by:  hb3an  1918  vtocl3gaf  3162  mob  3267  reusv6OLD  4648  infpssrlem4  8689  axcc3  8821  axdc3lem4  8836  axdc4lem  8838  axacndlem4  8991  axacndlem5  8992  axacnd  8993  dedekind  9747  dedekindle  9748  nfcprod1  13699  nfcprod  13700  mreexexd  15027  gsumsnf  16959  gsummatr01lem4  19138  iuncon  19907  hasheuni  28069  measvunilem  28161  measvunilem0  28162  measvuni  28163  volfiniune  28180  dfon2lem1  29191  dfon2lem3  29193  nfwrecs  29314  upixp  30196  sdclem1  30212  rfcnnnub  31365  suprnmpt  31405  fmuldfeqlem1  31530  fmuldfeq  31531  fmul01lt1  31534  infrglb  31538  fprodle  31558  mullimc  31576  mullimcf  31583  limsupre  31601  addlimc  31608  0ellimcdiv  31609  dvmptfprodlem  31695  dvmptfprod  31696  dvnprodlem1  31697  iblspltprt  31726  stoweidlem16  31752  stoweidlem17  31753  stoweidlem19  31755  stoweidlem20  31756  stoweidlem22  31758  stoweidlem26  31762  stoweidlem28  31764  stoweidlem31  31767  stoweidlem34  31770  stoweidlem35  31771  stoweidlem48  31784  stoweidlem52  31788  stoweidlem53  31789  stoweidlem56  31792  stoweidlem57  31793  stoweidlem60  31796  fourierdlem73  31916  fourierdlem77  31920  fourierdlem83  31926  fourierdlem87  31930  etransclem32  32003  tratrb  33175  bnj919  33693  bnj1379  33757  bnj571  33832  bnj607  33842  bnj873  33850  bnj964  33869  bnj981  33876  bnj1123  33910  bnj1128  33914  bnj1204  33936  bnj1279  33942  bnj1388  33957  bnj1398  33958  bnj1417  33965  bnj1444  33967  bnj1445  33968  bnj1449  33972  bnj1489  33980  bnj1518  33988  bnj1525  33993  pmapglbx  35368  cdlemefr29exN  36003