Theorem nf3an 1902

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

Syntax hints:   ∧ wa 397   ∧ w3a 1087  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-ex 1780  df-nf 1784

This theorem is referenced by:  hb3an  2296  vtocl3gaf  3521  mob  3657  nffrecs  8130  nfwrecsOLD  8164  infpssrlem4  10108  axcc3  10240  axdc3lem4  10255  axdc4lem  10257  axacndlem4  10412  axacndlem5  10413  axacnd  10414  dedekind  11184  dedekindle  11185  nfcprod1  15665  nfcprod  15666  fprodle  15751  mreexexd  17402  gsumsnf  19599  gsummatr01lem4  21852  iunconn  22624  hasheuni  32098  measvunilem  32225  measvunilem0  32226  measvuni  32227  volfiniune  32243  bnj919  32792  bnj1379  32855  bnj571  32931  bnj607  32941  bnj873  32949  bnj964  32968  bnj981  32975  bnj1123  33011  bnj1128  33015  bnj1204  33037  bnj1279  33043  bnj1388  33058  bnj1398  33059  bnj1417  33066  bnj1444  33068  bnj1445  33069  bnj1449  33073  bnj1489  33081  bnj1518  33089  bnj1525  33094  dfon2lem1  33804  dfon2lem3  33806  isbasisrelowllem1  35570  isbasisrelowllem2  35571  poimirlem27  35848  upixp  35931  sdclem1  35945  pmapglbx  37825  cdlemefr29exN  38458  gneispace  41782  tratrb  42194  rfcnnnub  42617  uzwo4  42639  suprnmpt  42754  choicefi  42784  iunmapsn  42801  infxr  42954  rexabslelem  43006  fsumiunss  43165  fmuldfeqlem1  43172  fmuldfeq  43173  fmul01lt1  43176  mullimc  43206  mullimcf  43213  limsupre  43231  addlimc  43238  0ellimcdiv  43239  fnlimfvre  43264  climinf2mpt  43304  climinfmpt  43305  limsupmnfuzlem  43316  dvmptfprodlem  43534  dvmptfprod  43535  dvnprodlem1  43536  iblspltprt  43563  stoweidlem16  43606  stoweidlem17  43607  stoweidlem19  43609  stoweidlem20  43610  stoweidlem22  43612  stoweidlem26  43616  stoweidlem28  43618  stoweidlem31  43621  stoweidlem34  43624  stoweidlem35  43625  stoweidlem48  43638  stoweidlem52  43642  stoweidlem53  43643  stoweidlem56  43646  stoweidlem57  43647  stoweidlem60  43650  fourierdlem73  43769  fourierdlem77  43773  fourierdlem83  43779  fourierdlem87  43783  etransclem32  43856  sge0pnffigt  43984  sge0iunmptlemre  44003  sge0iunmpt  44006  meaiininc2  44076  opnvonmbllem2  44221  issmfle  44333  issmfgt  44344  issmfge  44358  smflimlem2  44360  smflimmpt  44397  smfinflem  44404  smflimsuplem7  44413  smflimsuplem8  44414  smflimsupmpt  44416  smfliminfmpt  44419  ich2exprop  44981  ichnreuop  44982  2arymaptfo  46058