Theorem nf3an 1931

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

Syntax hints:   ∧ wa 400   ∧ w3a 1103  Ⅎwnf 1813

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-ex 1810  df-nf 1814

This theorem is referenced by:  hb3an  2336  mob  3681  nffrecs  8281  infpssrlem4  10291  axcc3  10423  axdc3lem4  10438  axdc4lem  10440  axacndlem4  10596  axacndlem5  10597  axacnd  10598  dedekind  11374  dedekindle  11375  nfcprod1  15964  nfcprod  15965  fprodle  16052  mreexexd  17705  gsumsnf  20024  gsummatr01lem4  22796  iunconn  23566  hasheuni  34456  measvunilem  34583  measvunilem0  34584  measvuni  34585  volfiniune  34601  bnj919  35137  bnj1379  35199  bnj571  35275  bnj607  35285  bnj873  35293  bnj964  35312  bnj981  35319  bnj1123  35355  bnj1128  35359  bnj1204  35381  bnj1279  35387  bnj1388  35402  bnj1398  35403  bnj1417  35410  bnj1444  35412  bnj1445  35413  bnj1449  35417  bnj1489  35425  bnj1518  35433  bnj1525  35438  dfon2lem1  36254  dfon2lem3  36256  axtcond  36970  isbasisrelowllem1  37982  isbasisrelowllem2  37983  poimirlem27  38279  upixp  38361  sdclem1  38375  pmapglbx  40524  cdlemefr29exN  41157  gneispace  44843  tratrb  45228  rfcnnnub  45739  uzwo4  45756  suprnmpt  45875  choicefi  45900  iunmapsn  45916  infxr  46065  rexabslelem  46115  fsumiunss  46274  fmuldfeqlem1  46281  fmuldfeq  46282  fmul01lt1  46285  mullimc  46315  mullimcf  46322  limsupre  46338  addlimc  46345  0ellimcdiv  46346  fnlimfvre  46371  climinf2mpt  46411  climinfmpt  46412  limsupmnfuzlem  46423  dvmptfprodlem  46641  dvmptfprod  46642  dvnprodlem1  46643  iblspltprt  46670  stoweidlem16  46713  stoweidlem17  46714  stoweidlem19  46716  stoweidlem20  46717  stoweidlem22  46719  stoweidlem26  46723  stoweidlem28  46725  stoweidlem31  46728  stoweidlem34  46731  stoweidlem35  46732  stoweidlem48  46745  stoweidlem52  46749  stoweidlem53  46750  stoweidlem56  46753  stoweidlem57  46754  stoweidlem60  46757  fourierdlem73  46876  fourierdlem77  46880  fourierdlem83  46886  fourierdlem87  46890  etransclem32  46963  sge0pnffigt  47093  sge0iunmptlemre  47112  sge0iunmpt  47115  meaiininc2  47185  opnvonmbllem2  47330  issmfle  47442  issmfgt  47453  issmfge  47467  smflimlem2  47469  smflimmpt  47507  smfinflem  47514  smflimsuplem7  47523  smflimsuplem8  47524  smflimsupmpt  47526  smfliminfmpt  47529  fsupdm  47539  finfdm  47543  ich2exprop  48203  ichnreuop  48204  2arymaptfo  49417