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  2334  mob  3675  nffrecs  8282  infpssrlem4  10308  axcc3  10440  axdc3lem4  10455  axdc4lem  10457  axacndlem4  10619  axacndlem5  10620  axacnd  10621  dedekind  11397  dedekindle  11398  nfcprod1  15997  nfcprod  15998  fprodle  16083  mreexexd  17736  gsumsnf  20080  gsummatr01lem4  22880  iunconn  23653  hasheuni  34595  measvunilem  34723  measvunilem0  34724  measvuni  34725  volfiniune  34741  bnj919  35277  bnj1379  35339  bnj571  35415  bnj607  35425  bnj873  35433  bnj964  35452  bnj981  35459  bnj1123  35495  bnj1128  35499  bnj1204  35521  bnj1279  35527  bnj1388  35542  bnj1398  35543  bnj1417  35550  bnj1444  35552  bnj1445  35553  bnj1449  35557  bnj1489  35565  bnj1518  35573  bnj1525  35578  dfon2lem1  36360  dfon2lem3  36362  axtcond  37097  isbasisrelowllem1  38109  isbasisrelowllem2  38110  poimirlem27  38396  upixp  38479  sdclem1  38493  pmapglbx  40642  cdlemefr29exN  41275  gneispace  44974  tratrb  45359  rfcnnnub  45870  uzwo4  45887  suprnmpt  46006  choicefi  46031  iunmapsn  46047  infxr  46196  rexabslelem  46246  fsumiunss  46405  fmuldfeqlem1  46412  fmuldfeq  46413  fmul01lt1  46416  mullimc  46446  mullimcf  46453  limsupre  46469  addlimc  46476  0ellimcdiv  46477  fnlimfvre  46502  climinf2mpt  46542  climinfmpt  46543  limsupmnfuzlem  46554  dvmptfprodlem  46772  dvmptfprod  46773  dvnprodlem1  46774  iblspltprt  46801  stoweidlem16  46844  stoweidlem17  46845  stoweidlem19  46847  stoweidlem20  46848  stoweidlem22  46850  stoweidlem26  46854  stoweidlem28  46856  stoweidlem31  46859  stoweidlem34  46862  stoweidlem35  46863  stoweidlem48  46876  stoweidlem52  46880  stoweidlem53  46881  stoweidlem56  46884  stoweidlem57  46885  stoweidlem60  46888  fourierdlem73  47007  fourierdlem77  47011  fourierdlem83  47017  fourierdlem87  47021  etransclem32  47094  sge0pnffigt  47224  sge0iunmptlemre  47243  sge0iunmpt  47246  meaiininc2  47316  opnvonmbllem2  47461  issmfle  47573  issmfgt  47584  issmfge  47598  smflimlem2  47600  smflimmpt  47638  smfinflem  47645  smflimsuplem7  47654  smflimsuplem8  47655  smflimsupmpt  47657  smfliminfmpt  47660  fsupdm  47670  finfdm  47674  ich2exprop  48371  ichnreuop  48372  2arymaptfo  49584