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 1088	. 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 395   ∧ w3a 1086  Ⅎwnf 1784

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-ex 1781  df-nf 1785

This theorem is referenced by:  hb3an  2307  vtocl3gafOLD  3537  mob  3675  nffrecs  8225  infpssrlem4  10216  axcc3  10348  axdc3lem4  10363  axdc4lem  10365  axacndlem4  10521  axacndlem5  10522  axacnd  10523  dedekind  11296  dedekindle  11297  nfcprod1  15831  nfcprod  15832  fprodle  15919  mreexexd  17571  gsumsnf  19882  gsummatr01lem4  22602  iunconn  23372  hasheuni  34242  measvunilem  34369  measvunilem0  34370  measvuni  34371  volfiniune  34387  bnj919  34923  bnj1379  34986  bnj571  35062  bnj607  35072  bnj873  35080  bnj964  35099  bnj981  35106  bnj1123  35142  bnj1128  35146  bnj1204  35168  bnj1279  35174  bnj1388  35189  bnj1398  35190  bnj1417  35197  bnj1444  35199  bnj1445  35200  bnj1449  35204  bnj1489  35212  bnj1518  35220  bnj1525  35225  dfon2lem1  35975  dfon2lem3  35977  isbasisrelowllem1  37560  isbasisrelowllem2  37561  poimirlem27  37848  upixp  37930  sdclem1  37944  pmapglbx  40029  cdlemefr29exN  40662  gneispace  44375  tratrb  44777  rfcnnnub  45281  uzwo4  45298  suprnmpt  45418  choicefi  45444  iunmapsn  45461  infxr  45611  rexabslelem  45662  fsumiunss  45821  fmuldfeqlem1  45828  fmuldfeq  45829  fmul01lt1  45832  mullimc  45862  mullimcf  45869  limsupre  45885  addlimc  45892  0ellimcdiv  45893  fnlimfvre  45918  climinf2mpt  45958  climinfmpt  45959  limsupmnfuzlem  45970  dvmptfprodlem  46188  dvmptfprod  46189  dvnprodlem1  46190  iblspltprt  46217  stoweidlem16  46260  stoweidlem17  46261  stoweidlem19  46263  stoweidlem20  46264  stoweidlem22  46266  stoweidlem26  46270  stoweidlem28  46272  stoweidlem31  46275  stoweidlem34  46278  stoweidlem35  46279  stoweidlem48  46292  stoweidlem52  46296  stoweidlem53  46297  stoweidlem56  46300  stoweidlem57  46301  stoweidlem60  46304  fourierdlem73  46423  fourierdlem77  46427  fourierdlem83  46433  fourierdlem87  46437  etransclem32  46510  sge0pnffigt  46640  sge0iunmptlemre  46659  sge0iunmpt  46662  meaiininc2  46732  opnvonmbllem2  46877  issmfle  46989  issmfgt  47000  issmfge  47014  smflimlem2  47016  smflimmpt  47054  smfinflem  47061  smflimsuplem7  47070  smflimsuplem8  47071  smflimsupmpt  47073  smfliminfmpt  47076  fsupdm  47086  finfdm  47090  ich2exprop  47717  ichnreuop  47718  2arymaptfo  48900