Theorem nf3an 1877

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

Syntax hints:   /\ wa 369   /\ w3a 973   F/wnf 1599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803

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

This theorem is referenced by:  hb3an  1879  vtocl3gaf  3180  mob  3285  reusv6OLD  4658  ovmpt3rab1  6516  infpssrlem4  8682  axcc3  8814  axdc3lem4  8829  axdc4lem  8831  axacndlem4  8984  axacndlem5  8985  axacnd  8986  dedekind  9739  dedekindle  9740  mreexexd  14899  gsumsnf  16771  gsummatr01lem4  18927  iuncon  19695  hasheuni  27731  measvunilem  27823  measvunilem0  27824  measvuni  27825  volfiniune  27842  nfcprod1  28619  nfcprod  28620  dfon2lem1  28792  dfon2lem3  28794  nfwrecs  28915  upixp  29823  sdclem1  29839  rfcnnnub  30989  suprnmpt  31029  fmuldfeqlem1  31132  fmuldfeq  31133  fmul01lt1  31136  infrglb  31140  mullimc  31158  mullimcf  31165  limsupre  31183  addlimc  31190  0ellimcdiv  31191  iblspltprt  31291  stoweidlem16  31316  stoweidlem17  31317  stoweidlem19  31319  stoweidlem20  31320  stoweidlem22  31322  stoweidlem26  31326  stoweidlem28  31328  stoweidlem31  31331  stoweidlem34  31334  stoweidlem35  31335  stoweidlem48  31348  stoweidlem52  31352  stoweidlem53  31353  stoweidlem56  31356  stoweidlem57  31357  stoweidlem60  31360  fourierdlem73  31480  fourierdlem77  31484  fourierdlem83  31490  fourierdlem87  31494  tratrb  32386  bnj919  32904  bnj1379  32968  bnj571  33043  bnj607  33053  bnj873  33061  bnj964  33080  bnj981  33087  bnj1123  33121  bnj1128  33125  bnj1204  33147  bnj1279  33153  bnj1388  33168  bnj1398  33169  bnj1417  33176  bnj1444  33178  bnj1445  33179  bnj1449  33183  bnj1489  33191  bnj1518  33199  bnj1525  33204  pmapglbx  34565  cdlemefr29exN  35198