Theorem nf3an 1934

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

This proof depends on syntax axioms:   ∧ wa 401   ∧ w3a 1103  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-nf 1817

This theorem is used by:  hb3an  2338  mob  3682  nffrecs  8282  infpssrlem4  10301  axcc3  10433  axdc3lem4  10448  axdc4lem  10450  axacndlem4  10606  axacndlem5  10607  axacnd  10608  dedekind  11384  dedekindle  11385  nfcprod1  15980  nfcprod  15981  fprodle  16068  mreexexd  17721  gsumsnf  20046  gsummatr01lem4  22844  iunconn  23614  hasheuni  34498  measvunilem  34626  measvunilem0  34627  measvuni  34628  volfiniune  34644  bnj919  35180  bnj1379  35242  bnj571  35318  bnj607  35328  bnj873  35336  bnj964  35355  bnj981  35362  bnj1123  35398  bnj1128  35402  bnj1204  35424  bnj1279  35430  bnj1388  35445  bnj1398  35446  bnj1417  35453  bnj1444  35455  bnj1445  35456  bnj1449  35460  bnj1489  35468  bnj1518  35476  bnj1525  35481  dfon2lem1  36286  dfon2lem3  36288  axtcond  37022  isbasisrelowllem1  38034  isbasisrelowllem2  38035  poimirlem27  38331  upixp  38413  sdclem1  38427  pmapglbx  40576  cdlemefr29exN  41209  gneispace  44893  tratrb  45278  rfcnnnub  45789  uzwo4  45806  suprnmpt  45925  choicefi  45950  iunmapsn  45966  infxr  46115  rexabslelem  46165  fsumiunss  46324  fmuldfeqlem1  46331  fmuldfeq  46332  fmul01lt1  46335  mullimc  46365  mullimcf  46372  limsupre  46388  addlimc  46395  0ellimcdiv  46396  fnlimfvre  46421  climinf2mpt  46461  climinfmpt  46462  limsupmnfuzlem  46473  dvmptfprodlem  46691  dvmptfprod  46692  dvnprodlem1  46693  iblspltprt  46720  stoweidlem16  46763  stoweidlem17  46764  stoweidlem19  46766  stoweidlem20  46767  stoweidlem22  46769  stoweidlem26  46773  stoweidlem28  46775  stoweidlem31  46778  stoweidlem34  46781  stoweidlem35  46782  stoweidlem48  46795  stoweidlem52  46799  stoweidlem53  46800  stoweidlem56  46803  stoweidlem57  46804  stoweidlem60  46807  fourierdlem73  46926  fourierdlem77  46930  fourierdlem83  46936  fourierdlem87  46940  etransclem32  47013  sge0pnffigt  47143  sge0iunmptlemre  47162  sge0iunmpt  47165  meaiininc2  47235  opnvonmbllem2  47380  issmfle  47492  issmfgt  47503  issmfge  47517  smflimlem2  47519  smflimmpt  47557  smfinflem  47564  smflimsuplem7  47573  smflimsuplem8  47574  smflimsupmpt  47576  smfliminfmpt  47579  fsupdm  47589  finfdm  47593  ich2exprop  48253  ichnreuop  48254  2arymaptfo  49467