Theorem nf3an 1908

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

Syntax hints:   ∧ wa 396   ∧ w3a 1092  Ⅎwnf 1790

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-ex 1787  df-nf 1791

This theorem is referenced by:  hb3an  2312  vtocl3gafOLD  3528  mob  3665  nffrecs  8230  infpssrlem4  10226  axcc3  10358  axdc3lem4  10373  axdc4lem  10375  axacndlem4  10531  axacndlem5  10532  axacnd  10533  dedekind  11307  dedekindle  11308  nfcprod1  15871  nfcprod  15872  fprodle  15959  mreexexd  17612  gsumsnf  19926  gsummatr01lem4  22648  iunconn  23418  hasheuni  34276  measvunilem  34403  measvunilem0  34404  measvuni  34405  volfiniune  34421  bnj919  34957  bnj1379  35019  bnj571  35095  bnj607  35105  bnj873  35113  bnj964  35132  bnj981  35139  bnj1123  35175  bnj1128  35179  bnj1204  35201  bnj1279  35207  bnj1388  35222  bnj1398  35223  bnj1417  35230  bnj1444  35232  bnj1445  35233  bnj1449  35237  bnj1489  35245  bnj1518  35253  bnj1525  35258  dfon2lem1  36016  dfon2lem3  36018  axtcond  36713  isbasisrelowllem1  37724  isbasisrelowllem2  37725  poimirlem27  38021  upixp  38103  sdclem1  38117  pmapglbx  40268  cdlemefr29exN  40901  gneispace  44585  tratrb  44987  rfcnnnub  45491  uzwo4  45508  suprnmpt  45628  choicefi  45653  iunmapsn  45669  infxr  45818  rexabslelem  45868  fsumiunss  46027  fmuldfeqlem1  46034  fmuldfeq  46035  fmul01lt1  46038  mullimc  46068  mullimcf  46075  limsupre  46091  addlimc  46098  0ellimcdiv  46099  fnlimfvre  46124  climinf2mpt  46164  climinfmpt  46165  limsupmnfuzlem  46176  dvmptfprodlem  46394  dvmptfprod  46395  dvnprodlem1  46396  iblspltprt  46423  stoweidlem16  46466  stoweidlem17  46467  stoweidlem19  46469  stoweidlem20  46470  stoweidlem22  46472  stoweidlem26  46476  stoweidlem28  46478  stoweidlem31  46481  stoweidlem34  46484  stoweidlem35  46485  stoweidlem48  46498  stoweidlem52  46502  stoweidlem53  46503  stoweidlem56  46506  stoweidlem57  46507  stoweidlem60  46510  fourierdlem73  46629  fourierdlem77  46633  fourierdlem83  46639  fourierdlem87  46643  etransclem32  46716  sge0pnffigt  46846  sge0iunmptlemre  46865  sge0iunmpt  46868  meaiininc2  46938  opnvonmbllem2  47083  issmfle  47195  issmfgt  47206  issmfge  47220  smflimlem2  47222  smflimmpt  47260  smfinflem  47267  smflimsuplem7  47276  smflimsuplem8  47277  smflimsupmpt  47279  smfliminfmpt  47282  fsupdm  47292  finfdm  47296  ich2exprop  47953  ichnreuop  47954  2arymaptfo  49152