Theorem nf3an 1819

Description: If 𝑥 is not free in 𝜑, 𝜓, and 𝜒, 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 1033	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		nfan.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3		nfan.2	. . . 4 ⊢ Ⅎ𝑥𝜓
4	2, 3	nfan 1816	. . 3 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)
5		nfan.3	. . 3 ⊢ Ⅎ𝑥𝜒
6	4, 5	nfan 1816	. 2 ⊢ Ⅎ𝑥((𝜑 ∧ 𝜓) ∧ 𝜒)
7	1, 6	nfxfr 1771	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓 ∧ 𝜒)

Syntax hints:   ∧ wa 383   ∧ w3a 1031  Ⅎwnf 1699

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

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701

This theorem is referenced by:  hb3an  2114  vtocl3gaf  3248  mob  3355  nfwrecs  7296  infpssrlem4  9011  axcc3  9143  axdc3lem4  9158  axdc4lem  9160  axacndlem4  9311  axacndlem5  9312  axacnd  9313  dedekind  10079  dedekindle  10080  nfcprod1  14479  nfcprod  14480  fprodle  14566  mreexexd  16131  mreexexdOLD  16132  gsumsnf  18176  gsummatr01lem4  20283  iuncon  21041  hasheuni  29474  measvunilem  29602  measvunilem0  29603  measvuni  29604  volfiniune  29620  bnj919  30091  bnj1379  30155  bnj571  30230  bnj607  30240  bnj873  30248  bnj964  30267  bnj981  30274  bnj1123  30308  bnj1128  30312  bnj1204  30334  bnj1279  30340  bnj1388  30355  bnj1398  30356  bnj1417  30363  bnj1444  30365  bnj1445  30366  bnj1449  30370  bnj1489  30378  bnj1518  30386  bnj1525  30391  dfon2lem1  30932  dfon2lem3  30934  isbasisrelowllem1  32379  isbasisrelowllem2  32380  poimirlem27  32606  upixp  32694  sdclem1  32709  pmapglbx  34073  cdlemefr29exN  34708  gneispace  37452  tratrb  37767  rfcnnnub  38218  uzwo4  38246  suprnmpt  38350  wessf1ornlem  38366  choicefi  38387  iunmapsn  38404  infxr  38524  fsumiunss  38642  fmuldfeqlem1  38649  fmuldfeq  38650  fmul01lt1  38653  mullimc  38683  mullimcf  38690  limsupre  38708  addlimc  38715  0ellimcdiv  38716  fnlimfvre  38741  dvmptfprodlem  38834  dvmptfprod  38835  dvnprodlem1  38836  iblspltprt  38865  stoweidlem16  38909  stoweidlem17  38910  stoweidlem19  38912  stoweidlem20  38913  stoweidlem22  38915  stoweidlem26  38919  stoweidlem28  38921  stoweidlem31  38924  stoweidlem34  38927  stoweidlem35  38928  stoweidlem48  38941  stoweidlem52  38945  stoweidlem53  38946  stoweidlem56  38949  stoweidlem57  38950  stoweidlem60  38953  fourierdlem73  39072  fourierdlem77  39076  fourierdlem83  39082  fourierdlem87  39086  etransclem32  39159  sge0pnffigt  39289  sge0iunmptlemre  39308  sge0iunmpt  39311  meaiininc2  39378  opnvonmbllem2  39523  issmfle  39632  issmfgt  39643  issmfge  39656  smflimlem2  39658