Theorem nf3an 1903

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

Syntax hints:   ∧ wa 395   ∧ w3a 1087  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-nf 1786

This theorem is referenced by:  hb3an  2308  vtocl3gafOLD  3525  mob  3663  nffrecs  8233  infpssrlem4  10228  axcc3  10360  axdc3lem4  10375  axdc4lem  10377  axacndlem4  10533  axacndlem5  10534  axacnd  10535  dedekind  11309  dedekindle  11310  nfcprod1  15873  nfcprod  15874  fprodle  15961  mreexexd  17614  gsumsnf  19928  gsummatr01lem4  22623  iunconn  23393  hasheuni  34229  measvunilem  34356  measvunilem0  34357  measvuni  34358  volfiniune  34374  bnj919  34910  bnj1379  34972  bnj571  35048  bnj607  35058  bnj873  35066  bnj964  35085  bnj981  35092  bnj1123  35128  bnj1128  35132  bnj1204  35154  bnj1279  35160  bnj1388  35175  bnj1398  35176  bnj1417  35183  bnj1444  35185  bnj1445  35186  bnj1449  35190  bnj1489  35198  bnj1518  35206  bnj1525  35211  dfon2lem1  35963  dfon2lem3  35965  axtcond  36660  isbasisrelowllem1  37671  isbasisrelowllem2  37672  poimirlem27  37968  upixp  38050  sdclem1  38064  pmapglbx  40215  cdlemefr29exN  40848  gneispace  44561  tratrb  44963  rfcnnnub  45467  uzwo4  45484  suprnmpt  45604  choicefi  45629  iunmapsn  45646  infxr  45796  rexabslelem  45846  fsumiunss  46005  fmuldfeqlem1  46012  fmuldfeq  46013  fmul01lt1  46016  mullimc  46046  mullimcf  46053  limsupre  46069  addlimc  46076  0ellimcdiv  46077  fnlimfvre  46102  climinf2mpt  46142  climinfmpt  46143  limsupmnfuzlem  46154  dvmptfprodlem  46372  dvmptfprod  46373  dvnprodlem1  46374  iblspltprt  46401  stoweidlem16  46444  stoweidlem17  46445  stoweidlem19  46447  stoweidlem20  46448  stoweidlem22  46450  stoweidlem26  46454  stoweidlem28  46456  stoweidlem31  46459  stoweidlem34  46462  stoweidlem35  46463  stoweidlem48  46476  stoweidlem52  46480  stoweidlem53  46481  stoweidlem56  46484  stoweidlem57  46485  stoweidlem60  46488  fourierdlem73  46607  fourierdlem77  46611  fourierdlem83  46617  fourierdlem87  46621  etransclem32  46694  sge0pnffigt  46824  sge0iunmptlemre  46843  sge0iunmpt  46846  meaiininc2  46916  opnvonmbllem2  47061  issmfle  47173  issmfgt  47184  issmfge  47198  smflimlem2  47200  smflimmpt  47238  smfinflem  47245  smflimsuplem7  47254  smflimsuplem8  47255  smflimsupmpt  47257  smfliminfmpt  47260  fsupdm  47270  finfdm  47274  ich2exprop  47931  ichnreuop  47932  2arymaptfo  49130