Theorem nf3an 1905

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

Syntax hints:   ∧ wa 397   ∧ w3a 1088  Ⅎwnf 1786

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-ex 1783  df-nf 1787

This theorem is referenced by:  hb3an  2298  vtocl3gaf  3569  mob  3714  nffrecs  8268  nfwrecsOLD  8302  infpssrlem4  10301  axcc3  10433  axdc3lem4  10448  axdc4lem  10450  axacndlem4  10605  axacndlem5  10606  axacnd  10607  dedekind  11377  dedekindle  11378  nfcprod1  15854  nfcprod  15855  fprodle  15940  mreexexd  17592  gsumsnf  19821  gsummatr01lem4  22160  iunconn  22932  hasheuni  33083  measvunilem  33210  measvunilem0  33211  measvuni  33212  volfiniune  33228  bnj919  33778  bnj1379  33841  bnj571  33917  bnj607  33927  bnj873  33935  bnj964  33954  bnj981  33961  bnj1123  33997  bnj1128  34001  bnj1204  34023  bnj1279  34029  bnj1388  34044  bnj1398  34045  bnj1417  34052  bnj1444  34054  bnj1445  34055  bnj1449  34059  bnj1489  34067  bnj1518  34075  bnj1525  34080  dfon2lem1  34755  dfon2lem3  34757  isbasisrelowllem1  36236  isbasisrelowllem2  36237  poimirlem27  36515  upixp  36597  sdclem1  36611  pmapglbx  38640  cdlemefr29exN  39273  gneispace  42885  tratrb  43297  rfcnnnub  43720  uzwo4  43740  suprnmpt  43870  choicefi  43899  iunmapsn  43916  infxr  44077  rexabslelem  44128  fsumiunss  44291  fmuldfeqlem1  44298  fmuldfeq  44299  fmul01lt1  44302  mullimc  44332  mullimcf  44339  limsupre  44357  addlimc  44364  0ellimcdiv  44365  fnlimfvre  44390  climinf2mpt  44430  climinfmpt  44431  limsupmnfuzlem  44442  dvmptfprodlem  44660  dvmptfprod  44661  dvnprodlem1  44662  iblspltprt  44689  stoweidlem16  44732  stoweidlem17  44733  stoweidlem19  44735  stoweidlem20  44736  stoweidlem22  44738  stoweidlem26  44742  stoweidlem28  44744  stoweidlem31  44747  stoweidlem34  44750  stoweidlem35  44751  stoweidlem48  44764  stoweidlem52  44768  stoweidlem53  44769  stoweidlem56  44772  stoweidlem57  44773  stoweidlem60  44776  fourierdlem73  44895  fourierdlem77  44899  fourierdlem83  44905  fourierdlem87  44909  etransclem32  44982  sge0pnffigt  45112  sge0iunmptlemre  45131  sge0iunmpt  45134  meaiininc2  45204  opnvonmbllem2  45349  issmfle  45461  issmfgt  45472  issmfge  45486  smflimlem2  45488  smflimmpt  45526  smfinflem  45533  smflimsuplem7  45542  smflimsuplem8  45543  smflimsupmpt  45545  smfliminfmpt  45548  fsupdm  45558  finfdm  45562  ich2exprop  46139  ichnreuop  46140  2arymaptfo  47340