Theorem nf3an 1904

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

Syntax hints:   ∧ wa 396   ∧ 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 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-ex 1782  df-nf 1786

This theorem is referenced by:  hb3an  2297  vtocl3gaf  3568  mob  3712  nffrecs  8264  nfwrecsOLD  8298  infpssrlem4  10297  axcc3  10429  axdc3lem4  10444  axdc4lem  10446  axacndlem4  10601  axacndlem5  10602  axacnd  10603  dedekind  11373  dedekindle  11374  nfcprod1  15850  nfcprod  15851  fprodle  15936  mreexexd  17588  gsumsnf  19815  gsummatr01lem4  22151  iunconn  22923  hasheuni  33071  measvunilem  33198  measvunilem0  33199  measvuni  33200  volfiniune  33216  bnj919  33766  bnj1379  33829  bnj571  33905  bnj607  33915  bnj873  33923  bnj964  33942  bnj981  33949  bnj1123  33985  bnj1128  33989  bnj1204  34011  bnj1279  34017  bnj1388  34032  bnj1398  34033  bnj1417  34040  bnj1444  34042  bnj1445  34043  bnj1449  34047  bnj1489  34055  bnj1518  34063  bnj1525  34068  dfon2lem1  34743  dfon2lem3  34745  isbasisrelowllem1  36224  isbasisrelowllem2  36225  poimirlem27  36503  upixp  36585  sdclem1  36599  pmapglbx  38628  cdlemefr29exN  39261  gneispace  42870  tratrb  43282  rfcnnnub  43705  uzwo4  43725  suprnmpt  43855  choicefi  43884  iunmapsn  43901  infxr  44063  rexabslelem  44114  fsumiunss  44277  fmuldfeqlem1  44284  fmuldfeq  44285  fmul01lt1  44288  mullimc  44318  mullimcf  44325  limsupre  44343  addlimc  44350  0ellimcdiv  44351  fnlimfvre  44376  climinf2mpt  44416  climinfmpt  44417  limsupmnfuzlem  44428  dvmptfprodlem  44646  dvmptfprod  44647  dvnprodlem1  44648  iblspltprt  44675  stoweidlem16  44718  stoweidlem17  44719  stoweidlem19  44721  stoweidlem20  44722  stoweidlem22  44724  stoweidlem26  44728  stoweidlem28  44730  stoweidlem31  44733  stoweidlem34  44736  stoweidlem35  44737  stoweidlem48  44750  stoweidlem52  44754  stoweidlem53  44755  stoweidlem56  44758  stoweidlem57  44759  stoweidlem60  44762  fourierdlem73  44881  fourierdlem77  44885  fourierdlem83  44891  fourierdlem87  44895  etransclem32  44968  sge0pnffigt  45098  sge0iunmptlemre  45117  sge0iunmpt  45120  meaiininc2  45190  opnvonmbllem2  45335  issmfle  45447  issmfgt  45458  issmfge  45472  smflimlem2  45474  smflimmpt  45512  smfinflem  45519  smflimsuplem7  45528  smflimsuplem8  45529  smflimsupmpt  45531  smfliminfmpt  45534  fsupdm  45544  finfdm  45548  ich2exprop  46125  ichnreuop  46126  2arymaptfo  47293