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  2303  vtocl3gafOLD  3533  mob  3671  nffrecs  8208  infpssrlem4  10192  axcc3  10324  axdc3lem4  10339  axdc4lem  10341  axacndlem4  10496  axacndlem5  10497  axacnd  10498  dedekind  11271  dedekindle  11272  nfcprod1  15810  nfcprod  15811  fprodle  15898  mreexexd  17549  gsumsnf  19860  gsummatr01lem4  22568  iunconn  23338  hasheuni  34090  measvunilem  34217  measvunilem0  34218  measvuni  34219  volfiniune  34235  bnj919  34771  bnj1379  34834  bnj571  34910  bnj607  34920  bnj873  34928  bnj964  34947  bnj981  34954  bnj1123  34990  bnj1128  34994  bnj1204  35016  bnj1279  35022  bnj1388  35037  bnj1398  35038  bnj1417  35045  bnj1444  35047  bnj1445  35048  bnj1449  35052  bnj1489  35060  bnj1518  35068  bnj1525  35073  dfon2lem1  35817  dfon2lem3  35819  isbasisrelowllem1  37389  isbasisrelowllem2  37390  poimirlem27  37687  upixp  37769  sdclem1  37783  pmapglbx  39808  cdlemefr29exN  40441  gneispace  44167  tratrb  44569  rfcnnnub  45073  uzwo4  45090  suprnmpt  45211  choicefi  45237  iunmapsn  45254  infxr  45405  rexabslelem  45456  fsumiunss  45615  fmuldfeqlem1  45622  fmuldfeq  45623  fmul01lt1  45626  mullimc  45656  mullimcf  45663  limsupre  45679  addlimc  45686  0ellimcdiv  45687  fnlimfvre  45712  climinf2mpt  45752  climinfmpt  45753  limsupmnfuzlem  45764  dvmptfprodlem  45982  dvmptfprod  45983  dvnprodlem1  45984  iblspltprt  46011  stoweidlem16  46054  stoweidlem17  46055  stoweidlem19  46057  stoweidlem20  46058  stoweidlem22  46060  stoweidlem26  46064  stoweidlem28  46066  stoweidlem31  46069  stoweidlem34  46072  stoweidlem35  46073  stoweidlem48  46086  stoweidlem52  46090  stoweidlem53  46091  stoweidlem56  46094  stoweidlem57  46095  stoweidlem60  46098  fourierdlem73  46217  fourierdlem77  46221  fourierdlem83  46227  fourierdlem87  46231  etransclem32  46304  sge0pnffigt  46434  sge0iunmptlemre  46453  sge0iunmpt  46456  meaiininc2  46526  opnvonmbllem2  46671  issmfle  46783  issmfgt  46794  issmfge  46808  smflimlem2  46810  smflimmpt  46848  smfinflem  46855  smflimsuplem7  46864  smflimsuplem8  46865  smflimsupmpt  46867  smfliminfmpt  46870  fsupdm  46880  finfdm  46884  ich2exprop  47502  ichnreuop  47503  2arymaptfo  48686