Theorem nf3an 1861

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

Syntax hints:   /\ wa 369   /\ w3a 958   F/wnf 1592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 960  df-ex 1590  df-nf 1593

This theorem is referenced by:  hb3an  1863  vtocl3gaf  3028  mob  3130  reusv6OLD  4491  infpssrlem4  8463  axcc3  8595  axdc3lem4  8610  axdc4lem  8612  axacndlem4  8764  axacndlem5  8765  axacnd  8766  dedekind  9520  dedekindle  9521  mreexexd  14568  gsummatr01lem4  18305  iuncon  18873  hasheuni  26387  measvunilem  26479  measvunilem0  26480  measvuni  26481  volfiniune  26499  nfcprod1  27269  nfcprod  27270  dfon2lem1  27442  dfon2lem3  27444  nfwrecs  27565  upixp  28464  sdclem1  28480  rfcnnnub  29600  fmuldfeqlem1  29605  fmuldfeq  29606  fmul01lt1  29609  infrglb  29614  stoweidlem16  29654  stoweidlem17  29655  stoweidlem19  29657  stoweidlem20  29658  stoweidlem22  29660  stoweidlem26  29664  stoweidlem28  29666  stoweidlem31  29669  stoweidlem34  29672  stoweidlem35  29673  stoweidlem48  29686  stoweidlem52  29690  stoweidlem53  29691  stoweidlem56  29694  stoweidlem57  29695  stoweidlem60  29698  ovmpt3rab1  30004  tratrb  30940  bnj919  31459  bnj1379  31523  bnj571  31598  bnj607  31608  bnj873  31616  bnj964  31635  bnj981  31642  bnj1123  31676  bnj1128  31680  bnj1204  31702  bnj1279  31708  bnj1388  31723  bnj1398  31724  bnj1417  31731  bnj1444  31733  bnj1445  31734  bnj1449  31738  bnj1489  31746  bnj1518  31754  bnj1525  31759  pmapglbx  32983  cdlemefr29exN  33616