Theorem nf3an 1831

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

Syntax hints:   /\ wa 384   /\ w3a 1037   F/wnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710

This theorem is referenced by:  hb3an  2129  vtocl3gaf  3275  mob  3388  nfwrecs  7409  infpssrlem4  9128  axcc3  9260  axdc3lem4  9275  axdc4lem  9277  axacndlem4  9432  axacndlem5  9433  axacnd  9434  dedekind  10200  dedekindle  10201  nfcprod1  14640  nfcprod  14641  fprodle  14727  mreexexd  16308  mreexexdOLD  16309  gsumsnf  18353  gsummatr01lem4  20464  iunconn  21231  hasheuni  30147  measvunilem  30275  measvunilem0  30276  measvuni  30277  volfiniune  30293  bnj919  30837  bnj1379  30901  bnj571  30976  bnj607  30986  bnj873  30994  bnj964  31013  bnj981  31020  bnj1123  31054  bnj1128  31058  bnj1204  31080  bnj1279  31086  bnj1388  31101  bnj1398  31102  bnj1417  31109  bnj1444  31111  bnj1445  31112  bnj1449  31116  bnj1489  31124  bnj1518  31132  bnj1525  31137  dfon2lem1  31688  dfon2lem3  31690  isbasisrelowllem1  33203  isbasisrelowllem2  33204  poimirlem27  33436  upixp  33524  sdclem1  33539  pmapglbx  35055  cdlemefr29exN  35690  gneispace  38432  tratrb  38746  rfcnnnub  39195  uzwo4  39221  suprnmpt  39355  wessf1ornlem  39371  choicefi  39392  iunmapsn  39409  infxr  39583  rexabslelem  39645  fsumiunss  39807  fmuldfeqlem1  39814  fmuldfeq  39815  fmul01lt1  39818  mullimc  39848  mullimcf  39855  limsupre  39873  addlimc  39880  0ellimcdiv  39881  fnlimfvre  39906  climinf2mpt  39946  climinfmpt  39947  limsupmnfuzlem  39958  dvmptfprodlem  40159  dvmptfprod  40160  dvnprodlem1  40161  iblspltprt  40189  stoweidlem16  40233  stoweidlem17  40234  stoweidlem19  40236  stoweidlem20  40237  stoweidlem22  40239  stoweidlem26  40243  stoweidlem28  40245  stoweidlem31  40248  stoweidlem34  40251  stoweidlem35  40252  stoweidlem48  40265  stoweidlem52  40269  stoweidlem53  40270  stoweidlem56  40273  stoweidlem57  40274  stoweidlem60  40277  fourierdlem73  40396  fourierdlem77  40400  fourierdlem83  40406  fourierdlem87  40410  etransclem32  40483  sge0pnffigt  40613  sge0iunmptlemre  40632  sge0iunmpt  40635  meaiininc2  40702  opnvonmbllem2  40847  issmfle  40954  issmfgt  40965  issmfge  40978  smflimlem2  40980  smflimmpt  41016  smfinflem  41023  smflimsuplem7  41032  smflimsuplem8  41033  smflimsupmpt  41035  smfliminfmpt  41038