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 1085	. 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 1853	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓 ∧ 𝜒)

Syntax hints:   ∧ wa 398   ∧ w3a 1083  Ⅎ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 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785

This theorem is referenced by:  hb3an  2309  vtocl3gaf  3577  mob  3708  nfwrecs  7949  infpssrlem4  9728  axcc3  9860  axdc3lem4  9875  axdc4lem  9877  axacndlem4  10032  axacndlem5  10033  axacnd  10034  dedekind  10803  dedekindle  10804  nfcprod1  15264  nfcprod  15265  fprodle  15350  mreexexd  16919  gsumsnf  19073  gsummatr01lem4  21267  iunconn  22036  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  34639  isbasisrelowllem2  34640  poimirlem27  34934  upixp  35019  sdclem1  35033  pmapglbx  36920  cdlemefr29exN  37553  gneispace  40504  tratrb  40890  rfcnnnub  41313  uzwo4  41335  suprnmpt  41450  choicefi  41483  iunmapsn  41500  infxr  41655  rexabslelem  41712  fsumiunss  41876  fmuldfeqlem1  41883  fmuldfeq  41884  fmul01lt1  41887  mullimc  41917  mullimcf  41924  limsupre  41942  addlimc  41949  0ellimcdiv  41950  fnlimfvre  41975  climinf2mpt  42015  climinfmpt  42016  limsupmnfuzlem  42027  dvmptfprodlem  42249  dvmptfprod  42250  dvnprodlem1  42251  iblspltprt  42278  stoweidlem16  42321  stoweidlem17  42322  stoweidlem19  42324  stoweidlem20  42325  stoweidlem22  42327  stoweidlem26  42331  stoweidlem28  42333  stoweidlem31  42336  stoweidlem34  42339  stoweidlem35  42340  stoweidlem48  42353  stoweidlem52  42357  stoweidlem53  42358  stoweidlem56  42361  stoweidlem57  42362  stoweidlem60  42365  fourierdlem73  42484  fourierdlem77  42488  fourierdlem83  42494  fourierdlem87  42498  etransclem32  42571  sge0pnffigt  42698  sge0iunmptlemre  42717  sge0iunmpt  42720  meaiininc2  42790  opnvonmbllem2  42935  issmfle  43042  issmfgt  43053  issmfge  43066  smflimlem2  43068  smflimmpt  43104  smfinflem  43111  smflimsuplem7  43120  smflimsuplem8  43121  smflimsupmpt  43123  smfliminfmpt  43126  ich2exprop  43653  ichnreuop  43654