Theorem nf3an 1928

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

Syntax hints:   ∧ wa 400   ∧ w3a 1101  Ⅎwnf 1810

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-ex 1807  df-nf 1811

This theorem is referenced by:  hb3an  2342  mob  3689  nffrecs  8276  infpssrlem4  10286  axcc3  10418  axdc3lem4  10433  axdc4lem  10435  axacndlem4  10591  axacndlem5  10592  axacnd  10593  dedekind  11369  dedekindle  11370  nfcprod1  15958  nfcprod  15959  fprodle  16046  mreexexd  17700  gsumsnf  20019  gsummatr01lem4  22780  iunconn  23550  hasheuni  34416  measvunilem  34543  measvunilem0  34544  measvuni  34545  volfiniune  34561  bnj919  35097  bnj1379  35159  bnj571  35235  bnj607  35245  bnj873  35253  bnj964  35272  bnj981  35279  bnj1123  35315  bnj1128  35319  bnj1204  35341  bnj1279  35347  bnj1388  35362  bnj1398  35363  bnj1417  35370  bnj1444  35372  bnj1445  35373  bnj1449  35377  bnj1489  35385  bnj1518  35393  bnj1525  35398  dfon2lem1  36168  dfon2lem3  36170  axtcond  36874  isbasisrelowllem1  37884  isbasisrelowllem2  37885  poimirlem27  38181  upixp  38263  sdclem1  38277  pmapglbx  40428  cdlemefr29exN  41061  gneispace  44745  tratrb  45130  rfcnnnub  45641  uzwo4  45658  suprnmpt  45777  choicefi  45802  iunmapsn  45818  infxr  45967  rexabslelem  46017  fsumiunss  46176  fmuldfeqlem1  46183  fmuldfeq  46184  fmul01lt1  46187  mullimc  46217  mullimcf  46224  limsupre  46240  addlimc  46247  0ellimcdiv  46248  fnlimfvre  46273  climinf2mpt  46313  climinfmpt  46314  limsupmnfuzlem  46325  dvmptfprodlem  46543  dvmptfprod  46544  dvnprodlem1  46545  iblspltprt  46572  stoweidlem16  46615  stoweidlem17  46616  stoweidlem19  46618  stoweidlem20  46619  stoweidlem22  46621  stoweidlem26  46625  stoweidlem28  46627  stoweidlem31  46630  stoweidlem34  46633  stoweidlem35  46634  stoweidlem48  46647  stoweidlem52  46651  stoweidlem53  46652  stoweidlem56  46655  stoweidlem57  46656  stoweidlem60  46659  fourierdlem73  46778  fourierdlem77  46782  fourierdlem83  46788  fourierdlem87  46792  etransclem32  46865  sge0pnffigt  46995  sge0iunmptlemre  47014  sge0iunmpt  47017  meaiininc2  47087  opnvonmbllem2  47232  issmfle  47344  issmfgt  47355  issmfge  47369  smflimlem2  47371  smflimmpt  47409  smfinflem  47416  smflimsuplem7  47425  smflimsuplem8  47426  smflimsupmpt  47428  smfliminfmpt  47431  fsupdm  47441  finfdm  47445  ich2exprop  48102  ichnreuop  48103  2arymaptfo  49312