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 1086	. 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 1854	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓 ∧ 𝜒)

Syntax hints:   ∧ wa 399   ∧ w3a 1084  Ⅎ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 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786

This theorem is referenced by:  hb3an  2305  vtocl3gaf  3525  mob  3656  nfwrecs  7932  infpssrlem4  9717  axcc3  9849  axdc3lem4  9864  axdc4lem  9866  axacndlem4  10021  axacndlem5  10022  axacnd  10023  dedekind  10792  dedekindle  10793  nfcprod1  15256  nfcprod  15257  fprodle  15342  mreexexd  16911  gsumsnf  19066  gsummatr01lem4  21263  iunconn  22033  hasheuni  31454  measvunilem  31581  measvunilem0  31582  measvuni  31583  volfiniune  31599  bnj919  32148  bnj1379  32212  bnj571  32288  bnj607  32298  bnj873  32306  bnj964  32325  bnj981  32332  bnj1123  32368  bnj1128  32372  bnj1204  32394  bnj1279  32400  bnj1388  32415  bnj1398  32416  bnj1417  32423  bnj1444  32425  bnj1445  32426  bnj1449  32430  bnj1489  32438  bnj1518  32446  bnj1525  32451  dfon2lem1  33141  dfon2lem3  33143  nffrecs  33233  isbasisrelowllem1  34772  isbasisrelowllem2  34773  poimirlem27  35084  upixp  35167  sdclem1  35181  pmapglbx  37065  cdlemefr29exN  37698  gneispace  40837  tratrb  41242  rfcnnnub  41665  uzwo4  41687  suprnmpt  41798  choicefi  41829  iunmapsn  41846  infxr  41999  rexabslelem  42055  fsumiunss  42217  fmuldfeqlem1  42224  fmuldfeq  42225  fmul01lt1  42228  mullimc  42258  mullimcf  42265  limsupre  42283  addlimc  42290  0ellimcdiv  42291  fnlimfvre  42316  climinf2mpt  42356  climinfmpt  42357  limsupmnfuzlem  42368  dvmptfprodlem  42586  dvmptfprod  42587  dvnprodlem1  42588  iblspltprt  42615  stoweidlem16  42658  stoweidlem17  42659  stoweidlem19  42661  stoweidlem20  42662  stoweidlem22  42664  stoweidlem26  42668  stoweidlem28  42670  stoweidlem31  42673  stoweidlem34  42676  stoweidlem35  42677  stoweidlem48  42690  stoweidlem52  42694  stoweidlem53  42695  stoweidlem56  42698  stoweidlem57  42699  stoweidlem60  42702  fourierdlem73  42821  fourierdlem77  42825  fourierdlem83  42831  fourierdlem87  42835  etransclem32  42908  sge0pnffigt  43035  sge0iunmptlemre  43054  sge0iunmpt  43057  meaiininc2  43127  opnvonmbllem2  43272  issmfle  43379  issmfgt  43390  issmfge  43403  smflimlem2  43405  smflimmpt  43441  smfinflem  43448  smflimsuplem7  43457  smflimsuplem8  43458  smflimsupmpt  43460  smfliminfmpt  43463  ich2exprop  43988  ichnreuop  43989  2arymaptfo  45068