Theorem nf3an 1898

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

Syntax hints:   ∧ wa 398   ∧ w3a 1083  Ⅎwnf 1780

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781

This theorem is referenced by:  hb3an  2305  vtocl3gaf  3576  mob  3707  nfwrecs  7948  infpssrlem4  9727  axcc3  9859  axdc3lem4  9874  axdc4lem  9876  axacndlem4  10031  axacndlem5  10032  axacnd  10033  dedekind  10802  dedekindle  10803  nfcprod1  15263  nfcprod  15264  fprodle  15349  mreexexd  16918  gsumsnf  19072  gsummatr01lem4  21266  iunconn  22035  hasheuni  31344  measvunilem  31471  measvunilem0  31472  measvuni  31473  volfiniune  31489  bnj919  32038  bnj1379  32102  bnj571  32178  bnj607  32188  bnj873  32196  bnj964  32215  bnj981  32222  bnj1123  32258  bnj1128  32262  bnj1204  32284  bnj1279  32290  bnj1388  32305  bnj1398  32306  bnj1417  32313  bnj1444  32315  bnj1445  32316  bnj1449  32320  bnj1489  32328  bnj1518  32336  bnj1525  32341  dfon2lem1  33028  dfon2lem3  33030  nffrecs  33120  isbasisrelowllem1  34635  isbasisrelowllem2  34636  poimirlem27  34918  upixp  35003  sdclem1  35017  pmapglbx  36904  cdlemefr29exN  37537  gneispace  40482  tratrb  40868  rfcnnnub  41291  uzwo4  41313  suprnmpt  41428  choicefi  41461  iunmapsn  41478  infxr  41633  rexabslelem  41690  fsumiunss  41854  fmuldfeqlem1  41861  fmuldfeq  41862  fmul01lt1  41865  mullimc  41895  mullimcf  41902  limsupre  41920  addlimc  41927  0ellimcdiv  41928  fnlimfvre  41953  climinf2mpt  41993  climinfmpt  41994  limsupmnfuzlem  42005  dvmptfprodlem  42227  dvmptfprod  42228  dvnprodlem1  42229  iblspltprt  42256  stoweidlem16  42300  stoweidlem17  42301  stoweidlem19  42303  stoweidlem20  42304  stoweidlem22  42306  stoweidlem26  42310  stoweidlem28  42312  stoweidlem31  42315  stoweidlem34  42318  stoweidlem35  42319  stoweidlem48  42332  stoweidlem52  42336  stoweidlem53  42337  stoweidlem56  42340  stoweidlem57  42341  stoweidlem60  42344  fourierdlem73  42463  fourierdlem77  42467  fourierdlem83  42473  fourierdlem87  42477  etransclem32  42550  sge0pnffigt  42677  sge0iunmptlemre  42696  sge0iunmpt  42699  meaiininc2  42769  opnvonmbllem2  42914  issmfle  43021  issmfgt  43032  issmfge  43045  smflimlem2  43047  smflimmpt  43083  smfinflem  43090  smflimsuplem7  43099  smflimsuplem8  43100  smflimsupmpt  43102  smfliminfmpt  43105  ich2exprop  43632  ichnreuop  43633