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  2335  mob  3675  nffrecs  8294  infpssrlem4  10377  axcc3  10509  axdc3lem4  10524  axdc4lem  10526  axacndlem4  10688  axacndlem5  10689  axacnd  10690  dedekind  11466  dedekindle  11467  nfcprod1  16070  nfcprod  16071  fprodle  16156  mreexexd  17815  gsumsnf  20160  gsummatr01lem4  22966  iunconn  23739  hasheuni  34710  measvunilem  34838  measvunilem0  34839  measvuni  34840  volfiniune  34856  bnj919  35391  bnj1379  35453  bnj571  35529  bnj607  35539  bnj873  35547  bnj964  35566  bnj981  35573  bnj1123  35609  bnj1128  35613  bnj1204  35635  bnj1279  35641  bnj1388  35656  bnj1398  35657  bnj1417  35664  bnj1444  35666  bnj1445  35667  bnj1449  35671  bnj1489  35679  bnj1518  35687  bnj1525  35692  dfon2lem1  36525  dfon2lem3  36527  axtcond  37246  isbasisrelowllem1  38258  isbasisrelowllem2  38259  poimirlem27  38545  upixp  38643  sdclem1  38657  pmapglbx  40806  cdlemefr29exN  41439  gneispace  45119  tratrb  45504  rfcnnnub  46022  uzwo4  46039  suprnmpt  46158  choicefi  46183  iunmapsn  46199  infxr  46347  rexabslelem  46397  fsumiunss  46556  fmuldfeqlem1  46563  fmuldfeq  46564  fmul01lt1  46567  mullimc  46597  mullimcf  46604  limsupre  46620  addlimc  46627  0ellimcdiv  46628  fnlimfvre  46653  climinf2mpt  46693  climinfmpt  46694  limsupmnfuzlem  46705  dvmptfprodlem  46923  dvmptfprod  46924  dvnprodlem1  46925  iblspltprt  46952  stoweidlem16  46995  stoweidlem17  46996  stoweidlem19  46998  stoweidlem20  46999  stoweidlem22  47001  stoweidlem26  47005  stoweidlem28  47007  stoweidlem31  47010  stoweidlem34  47013  stoweidlem35  47014  stoweidlem48  47027  stoweidlem52  47031  stoweidlem53  47032  stoweidlem56  47035  stoweidlem57  47036  stoweidlem60  47039  fourierdlem73  47158  fourierdlem77  47162  fourierdlem83  47168  fourierdlem87  47172  etransclem32  47245  sge0pnffigt  47375  sge0iunmptlemre  47394  sge0iunmpt  47397  meaiininc2  47467  opnvonmbllem2  47612  issmfle  47724  issmfgt  47735  issmfge  47749  smflimlem2  47751  smflimmpt  47789  smfinflem  47796  smflimsuplem7  47805  smflimsuplem8  47806  smflimsupmpt  47808  smfliminfmpt  47811  fsupdm  47821  finfdm  47825  ich2exprop  48522  ichnreuop  48523  2arymaptfo  49735