Theorem nf3an 2013

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

Syntax hints:   /\ wa 371   /\ w3a 985   F/wnf 1667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-12 1933

This theorem depends on definitions:  df-bi 189  df-an 373  df-3an 987  df-ex 1664  df-nf 1668

This theorem is referenced by:  hb3an  2015  vtocl3gaf  3116  mob  3220  nfwrecs  7030  infpssrlem4  8736  axcc3  8868  axdc3lem4  8883  axdc4lem  8885  axacndlem4  9035  axacndlem5  9036  axacnd  9037  dedekind  9797  dedekindle  9798  nfcprod1  13964  nfcprod  13965  fprodle  14050  mreexexd  15554  gsumsnf  17586  gsummatr01lem4  19683  iuncon  20443  hasheuni  28906  measvunilem  29034  measvunilem0  29035  measvuni  29036  volfiniune  29053  bnj919  29578  bnj1379  29642  bnj571  29717  bnj607  29727  bnj873  29735  bnj964  29754  bnj981  29761  bnj1123  29795  bnj1128  29799  bnj1204  29821  bnj1279  29827  bnj1388  29842  bnj1398  29843  bnj1417  29850  bnj1444  29852  bnj1445  29853  bnj1449  29857  bnj1489  29865  bnj1518  29873  bnj1525  29878  dfon2lem1  30429  dfon2lem3  30431  isbasisrelowllem1  31758  isbasisrelowllem2  31759  poimirlem27  31967  upixp  32056  sdclem1  32072  pmapglbx  33334  cdlemefr29exN  33969  tratrb  36897  rfcnnnub  37357  uzwo4  37392  suprnmpt  37439  wessf1ornlem  37459  choicefi  37481  fsumiunss  37654  fmuldfeqlem1  37660  fmuldfeq  37661  fmul01lt1  37664  infrglbOLD  37669  mullimc  37696  mullimcf  37703  limsupre  37721  limsupreOLD  37722  addlimc  37729  0ellimcdiv  37730  dvmptfprodlem  37819  dvmptfprod  37820  dvnprodlem1  37821  iblspltprt  37850  stoweidlem16  37876  stoweidlem17  37877  stoweidlem19  37879  stoweidlem20  37880  stoweidlem22  37882  stoweidlem26  37886  stoweidlem28  37888  stoweidlem31  37892  stoweidlem34  37895  stoweidlem35  37896  stoweidlem48  37909  stoweidlem52  37913  stoweidlem53  37914  stoweidlem56  37917  stoweidlem57  37918  stoweidlem60  37921  fourierdlem73  38043  fourierdlem77  38047  fourierdlem83  38053  fourierdlem87  38057  etransclem32  38131  sge0pnffigt  38238  sge0iunmptlemre  38257  sge0iunmpt  38260  opnvonmbllem2  38455