Theorem nf3an 1903

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

Syntax hints:   ∧ wa 395   ∧ w3a 1087  Ⅎ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 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-nf 1786

This theorem is referenced by:  hb3an  2308  vtocl3gafOLD  3538  mob  3676  nffrecs  8227  infpssrlem4  10220  axcc3  10352  axdc3lem4  10367  axdc4lem  10369  axacndlem4  10525  axacndlem5  10526  axacnd  10527  dedekind  11300  dedekindle  11301  nfcprod1  15835  nfcprod  15836  fprodle  15923  mreexexd  17575  gsumsnf  19886  gsummatr01lem4  22606  iunconn  23376  hasheuni  34223  measvunilem  34350  measvunilem0  34351  measvuni  34352  volfiniune  34368  bnj919  34904  bnj1379  34967  bnj571  35043  bnj607  35053  bnj873  35061  bnj964  35080  bnj981  35087  bnj1123  35123  bnj1128  35127  bnj1204  35149  bnj1279  35155  bnj1388  35170  bnj1398  35171  bnj1417  35178  bnj1444  35180  bnj1445  35181  bnj1449  35185  bnj1489  35193  bnj1518  35201  bnj1525  35206  dfon2lem1  35956  dfon2lem3  35958  isbasisrelowllem1  37531  isbasisrelowllem2  37532  poimirlem27  37819  upixp  37901  sdclem1  37915  pmapglbx  40066  cdlemefr29exN  40699  gneispace  44411  tratrb  44813  rfcnnnub  45317  uzwo4  45334  suprnmpt  45454  choicefi  45480  iunmapsn  45497  infxr  45647  rexabslelem  45698  fsumiunss  45857  fmuldfeqlem1  45864  fmuldfeq  45865  fmul01lt1  45868  mullimc  45898  mullimcf  45905  limsupre  45921  addlimc  45928  0ellimcdiv  45929  fnlimfvre  45954  climinf2mpt  45994  climinfmpt  45995  limsupmnfuzlem  46006  dvmptfprodlem  46224  dvmptfprod  46225  dvnprodlem1  46226  iblspltprt  46253  stoweidlem16  46296  stoweidlem17  46297  stoweidlem19  46299  stoweidlem20  46300  stoweidlem22  46302  stoweidlem26  46306  stoweidlem28  46308  stoweidlem31  46311  stoweidlem34  46314  stoweidlem35  46315  stoweidlem48  46328  stoweidlem52  46332  stoweidlem53  46333  stoweidlem56  46336  stoweidlem57  46337  stoweidlem60  46340  fourierdlem73  46459  fourierdlem77  46463  fourierdlem83  46469  fourierdlem87  46473  etransclem32  46546  sge0pnffigt  46676  sge0iunmptlemre  46695  sge0iunmpt  46698  meaiininc2  46768  opnvonmbllem2  46913  issmfle  47025  issmfgt  47036  issmfge  47050  smflimlem2  47052  smflimmpt  47090  smfinflem  47097  smflimsuplem7  47106  smflimsuplem8  47107  smflimsupmpt  47109  smfliminfmpt  47112  fsupdm  47122  finfdm  47126  ich2exprop  47753  ichnreuop  47754  2arymaptfo  48936