Theorem nf3an 1900

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

Syntax hints:   ∧ wa 395   ∧ w3a 1087  Ⅎwnf 1781

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-ex 1778  df-nf 1782

This theorem is referenced by:  hb3an  2305  vtocl3gafOLD  3594  mob  3739  nffrecs  8324  nfwrecsOLD  8358  infpssrlem4  10375  axcc3  10507  axdc3lem4  10522  axdc4lem  10524  axacndlem4  10679  axacndlem5  10680  axacnd  10681  dedekind  11453  dedekindle  11454  nfcprod1  15956  nfcprod  15957  fprodle  16044  mreexexd  17706  gsumsnf  19995  gsummatr01lem4  22685  iunconn  23457  hasheuni  34049  measvunilem  34176  measvunilem0  34177  measvuni  34178  volfiniune  34194  bnj919  34743  bnj1379  34806  bnj571  34882  bnj607  34892  bnj873  34900  bnj964  34919  bnj981  34926  bnj1123  34962  bnj1128  34966  bnj1204  34988  bnj1279  34994  bnj1388  35009  bnj1398  35010  bnj1417  35017  bnj1444  35019  bnj1445  35020  bnj1449  35024  bnj1489  35032  bnj1518  35040  bnj1525  35045  dfon2lem1  35747  dfon2lem3  35749  isbasisrelowllem1  37321  isbasisrelowllem2  37322  poimirlem27  37607  upixp  37689  sdclem1  37703  pmapglbx  39726  cdlemefr29exN  40359  gneispace  44096  tratrb  44507  rfcnnnub  44936  uzwo4  44955  suprnmpt  45081  choicefi  45107  iunmapsn  45124  infxr  45282  rexabslelem  45333  fsumiunss  45496  fmuldfeqlem1  45503  fmuldfeq  45504  fmul01lt1  45507  mullimc  45537  mullimcf  45544  limsupre  45562  addlimc  45569  0ellimcdiv  45570  fnlimfvre  45595  climinf2mpt  45635  climinfmpt  45636  limsupmnfuzlem  45647  dvmptfprodlem  45865  dvmptfprod  45866  dvnprodlem1  45867  iblspltprt  45894  stoweidlem16  45937  stoweidlem17  45938  stoweidlem19  45940  stoweidlem20  45941  stoweidlem22  45943  stoweidlem26  45947  stoweidlem28  45949  stoweidlem31  45952  stoweidlem34  45955  stoweidlem35  45956  stoweidlem48  45969  stoweidlem52  45973  stoweidlem53  45974  stoweidlem56  45977  stoweidlem57  45978  stoweidlem60  45981  fourierdlem73  46100  fourierdlem77  46104  fourierdlem83  46110  fourierdlem87  46114  etransclem32  46187  sge0pnffigt  46317  sge0iunmptlemre  46336  sge0iunmpt  46339  meaiininc2  46409  opnvonmbllem2  46554  issmfle  46666  issmfgt  46677  issmfge  46691  smflimlem2  46693  smflimmpt  46731  smfinflem  46738  smflimsuplem7  46747  smflimsuplem8  46748  smflimsupmpt  46750  smfliminfmpt  46753  fsupdm  46763  finfdm  46767  ich2exprop  47345  ichnreuop  47346  2arymaptfo  48388