Theorem nf3an 1901

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

Syntax hints:   ∧ wa 395   ∧ w3a 1086  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-nf 1784

This theorem is referenced by:  hb3an  2302  vtocl3gafOLD  3566  mob  3705  nffrecs  8287  nfwrecsOLD  8321  infpssrlem4  10325  axcc3  10457  axdc3lem4  10472  axdc4lem  10474  axacndlem4  10629  axacndlem5  10630  axacnd  10631  dedekind  11403  dedekindle  11404  nfcprod1  15929  nfcprod  15930  fprodle  16017  mreexexd  17665  gsumsnf  19939  gsummatr01lem4  22601  iunconn  23371  hasheuni  34121  measvunilem  34248  measvunilem0  34249  measvuni  34250  volfiniune  34266  bnj919  34803  bnj1379  34866  bnj571  34942  bnj607  34952  bnj873  34960  bnj964  34979  bnj981  34986  bnj1123  35022  bnj1128  35026  bnj1204  35048  bnj1279  35054  bnj1388  35069  bnj1398  35070  bnj1417  35077  bnj1444  35079  bnj1445  35080  bnj1449  35084  bnj1489  35092  bnj1518  35100  bnj1525  35105  dfon2lem1  35806  dfon2lem3  35808  isbasisrelowllem1  37378  isbasisrelowllem2  37379  poimirlem27  37676  upixp  37758  sdclem1  37772  pmapglbx  39793  cdlemefr29exN  40426  gneispace  44133  tratrb  44536  rfcnnnub  45040  uzwo4  45057  suprnmpt  45178  choicefi  45204  iunmapsn  45221  infxr  45374  rexabslelem  45425  fsumiunss  45584  fmuldfeqlem1  45591  fmuldfeq  45592  fmul01lt1  45595  mullimc  45625  mullimcf  45632  limsupre  45650  addlimc  45657  0ellimcdiv  45658  fnlimfvre  45683  climinf2mpt  45723  climinfmpt  45724  limsupmnfuzlem  45735  dvmptfprodlem  45953  dvmptfprod  45954  dvnprodlem1  45955  iblspltprt  45982  stoweidlem16  46025  stoweidlem17  46026  stoweidlem19  46028  stoweidlem20  46029  stoweidlem22  46031  stoweidlem26  46035  stoweidlem28  46037  stoweidlem31  46040  stoweidlem34  46043  stoweidlem35  46044  stoweidlem48  46057  stoweidlem52  46061  stoweidlem53  46062  stoweidlem56  46065  stoweidlem57  46066  stoweidlem60  46069  fourierdlem73  46188  fourierdlem77  46192  fourierdlem83  46198  fourierdlem87  46202  etransclem32  46275  sge0pnffigt  46405  sge0iunmptlemre  46424  sge0iunmpt  46427  meaiininc2  46497  opnvonmbllem2  46642  issmfle  46754  issmfgt  46765  issmfge  46779  smflimlem2  46781  smflimmpt  46819  smfinflem  46826  smflimsuplem7  46835  smflimsuplem8  46836  smflimsupmpt  46838  smfliminfmpt  46841  fsupdm  46851  finfdm  46855  ich2exprop  47465  ichnreuop  47466  2arymaptfo  48614