Theorem nf3an 1899

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

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

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-ex 1777  df-nf 1781

This theorem is referenced by:  hb3an  2300  vtocl3gafOLD  3582  mob  3726  nffrecs  8307  nfwrecsOLD  8341  infpssrlem4  10344  axcc3  10476  axdc3lem4  10491  axdc4lem  10493  axacndlem4  10648  axacndlem5  10649  axacnd  10650  dedekind  11422  dedekindle  11423  nfcprod1  15941  nfcprod  15942  fprodle  16029  mreexexd  17693  gsumsnf  19986  gsummatr01lem4  22680  iunconn  23452  hasheuni  34066  measvunilem  34193  measvunilem0  34194  measvuni  34195  volfiniune  34211  bnj919  34760  bnj1379  34823  bnj571  34899  bnj607  34909  bnj873  34917  bnj964  34936  bnj981  34943  bnj1123  34979  bnj1128  34983  bnj1204  35005  bnj1279  35011  bnj1388  35026  bnj1398  35027  bnj1417  35034  bnj1444  35036  bnj1445  35037  bnj1449  35041  bnj1489  35049  bnj1518  35057  bnj1525  35062  dfon2lem1  35765  dfon2lem3  35767  isbasisrelowllem1  37338  isbasisrelowllem2  37339  poimirlem27  37634  upixp  37716  sdclem1  37730  pmapglbx  39752  cdlemefr29exN  40385  gneispace  44124  tratrb  44534  rfcnnnub  44974  uzwo4  44993  suprnmpt  45117  choicefi  45143  iunmapsn  45160  infxr  45317  rexabslelem  45368  fsumiunss  45531  fmuldfeqlem1  45538  fmuldfeq  45539  fmul01lt1  45542  mullimc  45572  mullimcf  45579  limsupre  45597  addlimc  45604  0ellimcdiv  45605  fnlimfvre  45630  climinf2mpt  45670  climinfmpt  45671  limsupmnfuzlem  45682  dvmptfprodlem  45900  dvmptfprod  45901  dvnprodlem1  45902  iblspltprt  45929  stoweidlem16  45972  stoweidlem17  45973  stoweidlem19  45975  stoweidlem20  45976  stoweidlem22  45978  stoweidlem26  45982  stoweidlem28  45984  stoweidlem31  45987  stoweidlem34  45990  stoweidlem35  45991  stoweidlem48  46004  stoweidlem52  46008  stoweidlem53  46009  stoweidlem56  46012  stoweidlem57  46013  stoweidlem60  46016  fourierdlem73  46135  fourierdlem77  46139  fourierdlem83  46145  fourierdlem87  46149  etransclem32  46222  sge0pnffigt  46352  sge0iunmptlemre  46371  sge0iunmpt  46374  meaiininc2  46444  opnvonmbllem2  46589  issmfle  46701  issmfgt  46712  issmfge  46726  smflimlem2  46728  smflimmpt  46766  smfinflem  46773  smflimsuplem7  46782  smflimsuplem8  46783  smflimsupmpt  46785  smfliminfmpt  46788  fsupdm  46798  finfdm  46802  ich2exprop  47396  ichnreuop  47397  2arymaptfo  48504