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  2305  vtocl3gafOLD  3534  mob  3672  nffrecs  8222  infpssrlem4  10208  axcc3  10340  axdc3lem4  10355  axdc4lem  10357  axacndlem4  10512  axacndlem5  10513  axacnd  10514  dedekind  11287  dedekindle  11288  nfcprod1  15822  nfcprod  15823  fprodle  15910  mreexexd  17562  gsumsnf  19873  gsummatr01lem4  22593  iunconn  23363  hasheuni  34170  measvunilem  34297  measvunilem0  34298  measvuni  34299  volfiniune  34315  bnj919  34851  bnj1379  34914  bnj571  34990  bnj607  35000  bnj873  35008  bnj964  35027  bnj981  35034  bnj1123  35070  bnj1128  35074  bnj1204  35096  bnj1279  35102  bnj1388  35117  bnj1398  35118  bnj1417  35125  bnj1444  35127  bnj1445  35128  bnj1449  35132  bnj1489  35140  bnj1518  35148  bnj1525  35153  dfon2lem1  35897  dfon2lem3  35899  isbasisrelowllem1  37472  isbasisrelowllem2  37473  poimirlem27  37760  upixp  37842  sdclem1  37856  pmapglbx  39941  cdlemefr29exN  40574  gneispace  44291  tratrb  44693  rfcnnnub  45197  uzwo4  45214  suprnmpt  45334  choicefi  45360  iunmapsn  45377  infxr  45527  rexabslelem  45578  fsumiunss  45737  fmuldfeqlem1  45744  fmuldfeq  45745  fmul01lt1  45748  mullimc  45778  mullimcf  45785  limsupre  45801  addlimc  45808  0ellimcdiv  45809  fnlimfvre  45834  climinf2mpt  45874  climinfmpt  45875  limsupmnfuzlem  45886  dvmptfprodlem  46104  dvmptfprod  46105  dvnprodlem1  46106  iblspltprt  46133  stoweidlem16  46176  stoweidlem17  46177  stoweidlem19  46179  stoweidlem20  46180  stoweidlem22  46182  stoweidlem26  46186  stoweidlem28  46188  stoweidlem31  46191  stoweidlem34  46194  stoweidlem35  46195  stoweidlem48  46208  stoweidlem52  46212  stoweidlem53  46213  stoweidlem56  46216  stoweidlem57  46217  stoweidlem60  46220  fourierdlem73  46339  fourierdlem77  46343  fourierdlem83  46349  fourierdlem87  46353  etransclem32  46426  sge0pnffigt  46556  sge0iunmptlemre  46575  sge0iunmpt  46578  meaiininc2  46648  opnvonmbllem2  46793  issmfle  46905  issmfgt  46916  issmfge  46930  smflimlem2  46932  smflimmpt  46970  smfinflem  46977  smflimsuplem7  46986  smflimsuplem8  46987  smflimsupmpt  46989  smfliminfmpt  46992  fsupdm  47002  finfdm  47006  ich2exprop  47633  ichnreuop  47634  2arymaptfo  48816