Theorem nf3an 1936

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 1934	. . 3 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)
5		nfan.3	. . 3 ⊢ Ⅎ𝑥𝜒
6	4, 5	nfan 1934	. 2 ⊢ Ⅎ𝑥((𝜑 ∧ 𝜓) ∧ 𝜒)
7	1, 6	nfxfr 1886	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓 ∧ 𝜒)

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

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

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-nf 1817

This theorem is used by:  hb3anOLD  2338  mob  3678  nffrecs  8339  infpssrlem4  10423  axcc3  10555  axdc3lem4  10570  axdc4lem  10572  axacndlem4  10734  axacndlem5  10735  axacnd  10736  dedekind  11512  dedekindle  11513  nfcprod1  16121  nfcprod  16122  fprodle  16207  mreexexd  17872  gsumsnf  20218  gsummatr01lem4  23028  iunconn  23801  hasheuni  34828  measvunilem  34956  measvunilem0  34957  measvuni  34958  volfiniune  34974  bnj919  35509  bnj1379  35571  bnj571  35647  bnj607  35657  bnj873  35665  bnj964  35684  bnj981  35691  bnj1123  35727  bnj1128  35731  bnj1204  35753  bnj1279  35759  bnj1388  35774  bnj1398  35775  bnj1417  35782  bnj1444  35784  bnj1445  35785  bnj1449  35789  bnj1489  35797  bnj1518  35805  bnj1525  35810  srepdflem1  36126  srepdflem2  36127  dfon2lem3  36762  axtcond  37481  isbasisrelowllem1  38546  isbasisrelowllem2  38547  poimirlem27  38833  upixp  38931  sdclem1  38943  pmapglbx  41092  cdlemefr29exN  41725  gneispace  45395  tratrb  45779  rfcnnnub  46327  uzwo4  46344  suprnmpt  46462  choicefi  46487  iunmapsn  46503  infxr  46651  rexabslelem  46701  fsumiunss  46860  fmuldfeqlem1  46867  fmuldfeq  46868  fmul01lt1  46871  mullimc  46901  mullimcf  46908  limsupre  46924  addlimc  46931  0ellimcdiv  46932  fnlimfvre  46957  climinf2mpt  46997  climinfmpt  46998  limsupmnfuzlem  47009  dvmptfprodlem  47227  dvmptfprod  47228  dvnprodlem1  47229  iblspltprt  47256  stoweidlem16  47299  stoweidlem17  47300  stoweidlem19  47302  stoweidlem20  47303  stoweidlem22  47305  stoweidlem26  47309  stoweidlem28  47311  stoweidlem31  47314  stoweidlem34  47317  stoweidlem35  47318  stoweidlem48  47331  stoweidlem52  47335  stoweidlem53  47336  stoweidlem56  47339  stoweidlem57  47340  stoweidlem60  47343  fourierdlem73  47462  fourierdlem77  47466  fourierdlem83  47472  fourierdlem87  47476  etransclem32  47549  sge0pnffigt  47679  sge0iunmptlemre  47698  sge0iunmpt  47701  meaiininc2  47771  opnvonmbllem2  47916  issmfle  48028  issmfgt  48039  issmfge  48053  smflimlem2  48055  smflimmpt  48093  smfinflem  48100  smflimsuplem7  48109  smflimsuplem8  48110  smflimsupmpt  48112  smfliminfmpt  48115  fsupdm  48125  finfdm  48129  ich2exprop  48826  ichnreuop  48827  2arymaptfo  50097