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  3526  mob  3664  nffrecs  8226  infpssrlem4  10219  axcc3  10351  axdc3lem4  10366  axdc4lem  10368  axacndlem4  10524  axacndlem5  10525  axacnd  10526  dedekind  11300  dedekindle  11301  nfcprod1  15864  nfcprod  15865  fprodle  15952  mreexexd  17605  gsumsnf  19919  gsummatr01lem4  22633  iunconn  23403  hasheuni  34245  measvunilem  34372  measvunilem0  34373  measvuni  34374  volfiniune  34390  bnj919  34926  bnj1379  34988  bnj571  35064  bnj607  35074  bnj873  35082  bnj964  35101  bnj981  35108  bnj1123  35144  bnj1128  35148  bnj1204  35170  bnj1279  35176  bnj1388  35191  bnj1398  35192  bnj1417  35199  bnj1444  35201  bnj1445  35202  bnj1449  35206  bnj1489  35214  bnj1518  35222  bnj1525  35227  dfon2lem1  35979  dfon2lem3  35981  axtcond  36676  isbasisrelowllem1  37685  isbasisrelowllem2  37686  poimirlem27  37982  upixp  38064  sdclem1  38078  pmapglbx  40229  cdlemefr29exN  40862  gneispace  44579  tratrb  44981  rfcnnnub  45485  uzwo4  45502  suprnmpt  45622  choicefi  45647  iunmapsn  45664  infxr  45814  rexabslelem  45864  fsumiunss  46023  fmuldfeqlem1  46030  fmuldfeq  46031  fmul01lt1  46034  mullimc  46064  mullimcf  46071  limsupre  46087  addlimc  46094  0ellimcdiv  46095  fnlimfvre  46120  climinf2mpt  46160  climinfmpt  46161  limsupmnfuzlem  46172  dvmptfprodlem  46390  dvmptfprod  46391  dvnprodlem1  46392  iblspltprt  46419  stoweidlem16  46462  stoweidlem17  46463  stoweidlem19  46465  stoweidlem20  46466  stoweidlem22  46468  stoweidlem26  46472  stoweidlem28  46474  stoweidlem31  46477  stoweidlem34  46480  stoweidlem35  46481  stoweidlem48  46494  stoweidlem52  46498  stoweidlem53  46499  stoweidlem56  46502  stoweidlem57  46503  stoweidlem60  46506  fourierdlem73  46625  fourierdlem77  46629  fourierdlem83  46635  fourierdlem87  46639  etransclem32  46712  sge0pnffigt  46842  sge0iunmptlemre  46861  sge0iunmpt  46864  meaiininc2  46934  opnvonmbllem2  47079  issmfle  47191  issmfgt  47202  issmfge  47216  smflimlem2  47218  smflimmpt  47256  smfinflem  47263  smflimsuplem7  47272  smflimsuplem8  47273  smflimsupmpt  47275  smfliminfmpt  47278  fsupdm  47288  finfdm  47292  ich2exprop  47943  ichnreuop  47944  2arymaptfo  49142