Theorem nf3an 1933

Description: If 𝑥 is not free in 𝜑, 𝜓, and 𝜒, then it is not free in (𝜑 ∧ 𝜓 ∧ 𝜒). (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypotheses

Ref	Expression
nfan.1	⊢ Ⅎ𝑥𝜑
nfan.2	⊢ Ⅎ𝑥𝜓
nfan.3	⊢ Ⅎ𝑥𝜒

Assertion

Ref	Expression
nf3an	⊢ Ⅎ𝑥(𝜑 ∧ 𝜓 ∧ 𝜒)

Proof of Theorem nf3an

Step	Hyp	Ref	Expression
1		df-3an 1105	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		nfan.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3		nfan.2	. . . 4 ⊢ Ⅎ𝑥𝜓
4	2, 3	nfan 1931	. . 3 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)
5		nfan.3	. . 3 ⊢ Ⅎ𝑥𝜒
6	4, 5	nfan 1931	. 2 ⊢ Ⅎ𝑥((𝜑 ∧ 𝜓) ∧ 𝜒)
7	1, 6	nfxfr 1885	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓 ∧ 𝜒)

This proof depends on syntax axioms:   ∧ wa 401   ∧ w3a 1103  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-ex 1812  df-nf 1816

This theorem is used by:  hb3an  2334  mob  3674  nffrecs  8305  infpssrlem4  10388  axcc3  10520  axdc3lem4  10535  axdc4lem  10537  axacndlem4  10699  axacndlem5  10700  axacnd  10701  dedekind  11477  dedekindle  11478  nfcprod1  16083  nfcprod  16084  fprodle  16169  mreexexd  17828  gsumsnf  20173  gsummatr01lem4  22979  iunconn  23752  hasheuni  34764  measvunilem  34892  measvunilem0  34893  measvuni  34894  volfiniune  34910  bnj919  35445  bnj1379  35507  bnj571  35583  bnj607  35593  bnj873  35601  bnj964  35620  bnj981  35627  bnj1123  35663  bnj1128  35667  bnj1204  35689  bnj1279  35695  bnj1388  35710  bnj1398  35711  bnj1417  35718  bnj1444  35720  bnj1445  35721  bnj1449  35725  bnj1489  35733  bnj1518  35741  bnj1525  35746  srepdflem1  36005  srepdflem2  36006  dfon2lem3  36640  axtcond  37359  isbasisrelowllem1  38372  isbasisrelowllem2  38373  poimirlem27  38659  upixp  38757  sdclem1  38771  pmapglbx  40920  cdlemefr29exN  41553  gneispace  45228  tratrb  45613  rfcnnnub  46147  uzwo4  46164  suprnmpt  46283  choicefi  46308  iunmapsn  46324  infxr  46472  rexabslelem  46522  fsumiunss  46681  fmuldfeqlem1  46688  fmuldfeq  46689  fmul01lt1  46692  mullimc  46722  mullimcf  46729  limsupre  46745  addlimc  46752  0ellimcdiv  46753  fnlimfvre  46778  climinf2mpt  46818  climinfmpt  46819  limsupmnfuzlem  46830  dvmptfprodlem  47048  dvmptfprod  47049  dvnprodlem1  47050  iblspltprt  47077  stoweidlem16  47120  stoweidlem17  47121  stoweidlem19  47123  stoweidlem20  47124  stoweidlem22  47126  stoweidlem26  47130  stoweidlem28  47132  stoweidlem31  47135  stoweidlem34  47138  stoweidlem35  47139  stoweidlem48  47152  stoweidlem52  47156  stoweidlem53  47157  stoweidlem56  47160  stoweidlem57  47161  stoweidlem60  47164  fourierdlem73  47283  fourierdlem77  47287  fourierdlem83  47293  fourierdlem87  47297  etransclem32  47370  sge0pnffigt  47500  sge0iunmptlemre  47519  sge0iunmpt  47522  meaiininc2  47592  opnvonmbllem2  47737  issmfle  47849  issmfgt  47860  issmfge  47874  smflimlem2  47876  smflimmpt  47914  smfinflem  47921  smflimsuplem7  47930  smflimsuplem8  47931  smflimsupmpt  47933  smfliminfmpt  47936  fsupdm  47946  finfdm  47950  ich2exprop  48647  ichnreuop  48648  2arymaptfo  49860