Theorem nf3an 1863

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

Syntax hints:   /\ wa 369   /\ w3a 965   F/wnf 1589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792

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

This theorem is referenced by:  hb3an  1865  vtocl3gaf  3044  mob  3146  reusv6OLD  4508  infpssrlem4  8480  axcc3  8612  axdc3lem4  8627  axdc4lem  8629  axacndlem4  8782  axacndlem5  8783  axacnd  8784  dedekind  9538  dedekindle  9539  mreexexd  14591  gsummatr01lem4  18469  iuncon  19037  hasheuni  26539  measvunilem  26631  measvunilem0  26632  measvuni  26633  volfiniune  26651  nfcprod1  27428  nfcprod  27429  dfon2lem1  27601  dfon2lem3  27603  nfwrecs  27724  upixp  28628  sdclem1  28644  rfcnnnub  29763  fmuldfeqlem1  29768  fmuldfeq  29769  fmul01lt1  29772  infrglb  29776  stoweidlem16  29816  stoweidlem17  29817  stoweidlem19  29819  stoweidlem20  29820  stoweidlem22  29822  stoweidlem26  29826  stoweidlem28  29828  stoweidlem31  29831  stoweidlem34  29834  stoweidlem35  29835  stoweidlem48  29848  stoweidlem52  29852  stoweidlem53  29853  stoweidlem56  29856  stoweidlem57  29857  stoweidlem60  29860  ovmpt3rab1  30166  tratrb  31247  bnj919  31765  bnj1379  31829  bnj571  31904  bnj607  31914  bnj873  31922  bnj964  31941  bnj981  31948  bnj1123  31982  bnj1128  31986  bnj1204  32008  bnj1279  32014  bnj1388  32029  bnj1398  32030  bnj1417  32037  bnj1444  32039  bnj1445  32040  bnj1449  32044  bnj1489  32052  bnj1518  32060  bnj1525  32065  pmapglbx  33418  cdlemefr29exN  34051