Theorem nf3an 1986

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 984	. 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 1984	. . 3 |- F/ x ( ph /\ ps )
5		nfan.3	. . 3 |- F/ x ch
6	4, 5	nfan 1984	. 2 |- F/ x ( ( ph /\ ps ) /\ ch )
7	1, 6	nfxfr 1692	1 |- F/ x ( ph /\ ps /\ ch )

Syntax hints:   /\ wa 370   /\ w3a 982   F/wnf 1663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-12 1905

This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984  df-ex 1660  df-nf 1664

This theorem is referenced by:  hb3an  1988  vtocl3gaf  3148  mob  3253  nfwrecs  7035  infpssrlem4  8737  axcc3  8869  axdc3lem4  8884  axdc4lem  8886  axacndlem4  9036  axacndlem5  9037  axacnd  9038  dedekind  9798  dedekindle  9799  nfcprod1  13952  nfcprod  13953  fprodle  14038  mreexexd  15542  gsumsnf  17574  gsummatr01lem4  19670  iuncon  20430  hasheuni  28902  measvunilem  29030  measvunilem0  29031  measvuni  29032  volfiniune  29049  bnj919  29574  bnj1379  29638  bnj571  29713  bnj607  29723  bnj873  29731  bnj964  29750  bnj981  29757  bnj1123  29791  bnj1128  29795  bnj1204  29817  bnj1279  29823  bnj1388  29838  bnj1398  29839  bnj1417  29846  bnj1444  29848  bnj1445  29849  bnj1449  29853  bnj1489  29861  bnj1518  29869  bnj1525  29874  dfon2lem1  30424  dfon2lem3  30426  isbasisrelowllem1  31699  isbasisrelowllem2  31700  poimirlem27  31881  upixp  31970  sdclem1  31986  pmapglbx  33253  cdlemefr29exN  33888  tratrb  36755  rfcnnnub  37218  uzwo4  37254  suprnmpt  37288  wessf1ornlem  37309  fsumiunss  37477  fmuldfeqlem1  37480  fmuldfeq  37481  fmul01lt1  37484  infrglbOLD  37489  mullimc  37516  mullimcf  37523  limsupre  37541  limsupreOLD  37542  addlimc  37549  0ellimcdiv  37550  dvmptfprodlem  37639  dvmptfprod  37640  dvnprodlem1  37641  iblspltprt  37670  stoweidlem16  37696  stoweidlem17  37697  stoweidlem19  37699  stoweidlem20  37700  stoweidlem22  37702  stoweidlem26  37706  stoweidlem28  37708  stoweidlem31  37712  stoweidlem34  37715  stoweidlem35  37716  stoweidlem48  37729  stoweidlem52  37733  stoweidlem53  37734  stoweidlem56  37737  stoweidlem57  37738  stoweidlem60  37741  fourierdlem73  37863  fourierdlem77  37867  fourierdlem83  37873  fourierdlem87  37877  etransclem32  37951  sge0pnffigt  38026  sge0iunmptlemre  38045  sge0iunmpt  38048