Theorem nf3an 1920

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

Syntax hints:   ∧ wa 399   ∧ w3a 1097  Ⅎwnf 1802

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-ex 1799  df-nf 1803

This theorem is referenced by:  hb3an  2334  mob  3678  nffrecs  8258  infpssrlem4  10257  axcc3  10389  axdc3lem4  10404  axdc4lem  10406  axacndlem4  10562  axacndlem5  10563  axacnd  10564  dedekind  11340  dedekindle  11341  nfcprod1  15929  nfcprod  15930  fprodle  16017  mreexexd  17671  gsumsnf  19984  gsummatr01lem4  22706  iunconn  23476  hasheuni  34343  measvunilem  34470  measvunilem0  34471  measvuni  34472  volfiniune  34488  bnj919  35024  bnj1379  35086  bnj571  35162  bnj607  35172  bnj873  35180  bnj964  35199  bnj981  35206  bnj1123  35242  bnj1128  35246  bnj1204  35268  bnj1279  35274  bnj1388  35289  bnj1398  35290  bnj1417  35297  bnj1444  35299  bnj1445  35300  bnj1449  35304  bnj1489  35312  bnj1518  35320  bnj1525  35325  dfon2lem1  36092  dfon2lem3  36094  axtcond  36799  isbasisrelowllem1  37810  isbasisrelowllem2  37811  poimirlem27  38107  upixp  38189  sdclem1  38203  pmapglbx  40354  cdlemefr29exN  40987  gneispace  44671  tratrb  45073  rfcnnnub  45577  uzwo4  45594  suprnmpt  45713  choicefi  45738  iunmapsn  45754  infxr  45903  rexabslelem  45953  fsumiunss  46112  fmuldfeqlem1  46119  fmuldfeq  46120  fmul01lt1  46123  mullimc  46153  mullimcf  46160  limsupre  46176  addlimc  46183  0ellimcdiv  46184  fnlimfvre  46209  climinf2mpt  46249  climinfmpt  46250  limsupmnfuzlem  46261  dvmptfprodlem  46479  dvmptfprod  46480  dvnprodlem1  46481  iblspltprt  46508  stoweidlem16  46551  stoweidlem17  46552  stoweidlem19  46554  stoweidlem20  46555  stoweidlem22  46557  stoweidlem26  46561  stoweidlem28  46563  stoweidlem31  46566  stoweidlem34  46569  stoweidlem35  46570  stoweidlem48  46583  stoweidlem52  46587  stoweidlem53  46588  stoweidlem56  46591  stoweidlem57  46592  stoweidlem60  46595  fourierdlem73  46714  fourierdlem77  46718  fourierdlem83  46724  fourierdlem87  46728  etransclem32  46801  sge0pnffigt  46931  sge0iunmptlemre  46950  sge0iunmpt  46953  meaiininc2  47023  opnvonmbllem2  47168  issmfle  47280  issmfgt  47291  issmfge  47305  smflimlem2  47307  smflimmpt  47345  smfinflem  47352  smflimsuplem7  47361  smflimsuplem8  47362  smflimsupmpt  47364  smfliminfmpt  47367  fsupdm  47377  finfdm  47381  ich2exprop  48038  ichnreuop  48039  2arymaptfo  49237