Theorem nf3an 1930

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

This proof depends on syntax axioms:   ∧ wa 400   ∧ w3a 1102  Ⅎwnf 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-ex 1809  df-nf 1813

This theorem is used by:  hb3an  2335  mob  3679  nffrecs  8278  infpssrlem4  10296  axcc3  10428  axdc3lem4  10443  axdc4lem  10445  axacndlem4  10601  axacndlem5  10602  axacnd  10603  dedekind  11379  dedekindle  11380  nfcprod1  15969  nfcprod  15970  fprodle  16057  mreexexd  17710  gsumsnf  20029  gsummatr01lem4  22826  iunconn  23596  hasheuni  34484  measvunilem  34611  measvunilem0  34612  measvuni  34613  volfiniune  34629  bnj919  35165  bnj1379  35227  bnj571  35303  bnj607  35313  bnj873  35321  bnj964  35340  bnj981  35347  bnj1123  35383  bnj1128  35387  bnj1204  35409  bnj1279  35415  bnj1388  35430  bnj1398  35431  bnj1417  35438  bnj1444  35440  bnj1445  35441  bnj1449  35445  bnj1489  35453  bnj1518  35461  bnj1525  35466  dfon2lem1  36281  dfon2lem3  36283  axtcond  37017  isbasisrelowllem1  38029  isbasisrelowllem2  38030  poimirlem27  38326  upixp  38408  sdclem1  38422  pmapglbx  40571  cdlemefr29exN  41204  gneispace  44888  tratrb  45273  rfcnnnub  45784  uzwo4  45801  suprnmpt  45920  choicefi  45945  iunmapsn  45961  infxr  46110  rexabslelem  46160  fsumiunss  46319  fmuldfeqlem1  46326  fmuldfeq  46327  fmul01lt1  46330  mullimc  46360  mullimcf  46367  limsupre  46383  addlimc  46390  0ellimcdiv  46391  fnlimfvre  46416  climinf2mpt  46456  climinfmpt  46457  limsupmnfuzlem  46468  dvmptfprodlem  46686  dvmptfprod  46687  dvnprodlem1  46688  iblspltprt  46715  stoweidlem16  46758  stoweidlem17  46759  stoweidlem19  46761  stoweidlem20  46762  stoweidlem22  46764  stoweidlem26  46768  stoweidlem28  46770  stoweidlem31  46773  stoweidlem34  46776  stoweidlem35  46777  stoweidlem48  46790  stoweidlem52  46794  stoweidlem53  46795  stoweidlem56  46798  stoweidlem57  46799  stoweidlem60  46802  fourierdlem73  46921  fourierdlem77  46925  fourierdlem83  46931  fourierdlem87  46935  etransclem32  47008  sge0pnffigt  47138  sge0iunmptlemre  47157  sge0iunmpt  47160  meaiininc2  47230  opnvonmbllem2  47375  issmfle  47487  issmfgt  47498  issmfge  47512  smflimlem2  47514  smflimmpt  47552  smfinflem  47559  smflimsuplem7  47568  smflimsuplem8  47569  smflimsupmpt  47571  smfliminfmpt  47574  fsupdm  47584  finfdm  47588  ich2exprop  48248  ichnreuop  48249  2arymaptfo  49462