Theorem nf3an 1900

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

Syntax hints:   ∧ wa 395   ∧ w3a 1086  Ⅎwnf 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-ex 1779  df-nf 1783

This theorem is referenced by:  hb3an  2300  vtocl3gafOLD  3566  mob  3707  nffrecs  8291  nfwrecsOLD  8325  infpssrlem4  10329  axcc3  10461  axdc3lem4  10476  axdc4lem  10478  axacndlem4  10633  axacndlem5  10634  axacnd  10635  dedekind  11407  dedekindle  11408  nfcprod1  15927  nfcprod  15928  fprodle  16015  mreexexd  17667  gsumsnf  19944  gsummatr01lem4  22631  iunconn  23401  hasheuni  34027  measvunilem  34154  measvunilem0  34155  measvuni  34156  volfiniune  34172  bnj919  34722  bnj1379  34785  bnj571  34861  bnj607  34871  bnj873  34879  bnj964  34898  bnj981  34905  bnj1123  34941  bnj1128  34945  bnj1204  34967  bnj1279  34973  bnj1388  34988  bnj1398  34989  bnj1417  34996  bnj1444  34998  bnj1445  34999  bnj1449  35003  bnj1489  35011  bnj1518  35019  bnj1525  35024  dfon2lem1  35725  dfon2lem3  35727  isbasisrelowllem1  37297  isbasisrelowllem2  37298  poimirlem27  37595  upixp  37677  sdclem1  37691  pmapglbx  39712  cdlemefr29exN  40345  gneispace  44092  tratrb  44501  rfcnnnub  44986  uzwo4  45003  suprnmpt  45124  choicefi  45150  iunmapsn  45167  infxr  45323  rexabslelem  45374  fsumiunss  45535  fmuldfeqlem1  45542  fmuldfeq  45543  fmul01lt1  45546  mullimc  45576  mullimcf  45583  limsupre  45601  addlimc  45608  0ellimcdiv  45609  fnlimfvre  45634  climinf2mpt  45674  climinfmpt  45675  limsupmnfuzlem  45686  dvmptfprodlem  45904  dvmptfprod  45905  dvnprodlem1  45906  iblspltprt  45933  stoweidlem16  45976  stoweidlem17  45977  stoweidlem19  45979  stoweidlem20  45980  stoweidlem22  45982  stoweidlem26  45986  stoweidlem28  45988  stoweidlem31  45991  stoweidlem34  45994  stoweidlem35  45995  stoweidlem48  46008  stoweidlem52  46012  stoweidlem53  46013  stoweidlem56  46016  stoweidlem57  46017  stoweidlem60  46020  fourierdlem73  46139  fourierdlem77  46143  fourierdlem83  46149  fourierdlem87  46153  etransclem32  46226  sge0pnffigt  46356  sge0iunmptlemre  46375  sge0iunmpt  46378  meaiininc2  46448  opnvonmbllem2  46593  issmfle  46705  issmfgt  46716  issmfge  46730  smflimlem2  46732  smflimmpt  46770  smfinflem  46777  smflimsuplem7  46786  smflimsuplem8  46787  smflimsupmpt  46789  smfliminfmpt  46792  fsupdm  46802  finfdm  46806  ich2exprop  47404  ichnreuop  47405  2arymaptfo  48521