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  2301  vtocl3gafOLD  3545  mob  3685  nffrecs  8239  infpssrlem4  10235  axcc3  10367  axdc3lem4  10382  axdc4lem  10384  axacndlem4  10539  axacndlem5  10540  axacnd  10541  dedekind  11313  dedekindle  11314  nfcprod1  15850  nfcprod  15851  fprodle  15938  mreexexd  17585  gsumsnf  19859  gsummatr01lem4  22521  iunconn  23291  hasheuni  34048  measvunilem  34175  measvunilem0  34176  measvuni  34177  volfiniune  34193  bnj919  34730  bnj1379  34793  bnj571  34869  bnj607  34879  bnj873  34887  bnj964  34906  bnj981  34913  bnj1123  34949  bnj1128  34953  bnj1204  34975  bnj1279  34981  bnj1388  34996  bnj1398  34997  bnj1417  35004  bnj1444  35006  bnj1445  35007  bnj1449  35011  bnj1489  35019  bnj1518  35027  bnj1525  35032  dfon2lem1  35744  dfon2lem3  35746  isbasisrelowllem1  37316  isbasisrelowllem2  37317  poimirlem27  37614  upixp  37696  sdclem1  37710  pmapglbx  39736  cdlemefr29exN  40369  gneispace  44096  tratrb  44499  rfcnnnub  45003  uzwo4  45020  suprnmpt  45141  choicefi  45167  iunmapsn  45184  infxr  45336  rexabslelem  45387  fsumiunss  45546  fmuldfeqlem1  45553  fmuldfeq  45554  fmul01lt1  45557  mullimc  45587  mullimcf  45594  limsupre  45612  addlimc  45619  0ellimcdiv  45620  fnlimfvre  45645  climinf2mpt  45685  climinfmpt  45686  limsupmnfuzlem  45697  dvmptfprodlem  45915  dvmptfprod  45916  dvnprodlem1  45917  iblspltprt  45944  stoweidlem16  45987  stoweidlem17  45988  stoweidlem19  45990  stoweidlem20  45991  stoweidlem22  45993  stoweidlem26  45997  stoweidlem28  45999  stoweidlem31  46002  stoweidlem34  46005  stoweidlem35  46006  stoweidlem48  46019  stoweidlem52  46023  stoweidlem53  46024  stoweidlem56  46027  stoweidlem57  46028  stoweidlem60  46031  fourierdlem73  46150  fourierdlem77  46154  fourierdlem83  46160  fourierdlem87  46164  etransclem32  46237  sge0pnffigt  46367  sge0iunmptlemre  46386  sge0iunmpt  46389  meaiininc2  46459  opnvonmbllem2  46604  issmfle  46716  issmfgt  46727  issmfge  46741  smflimlem2  46743  smflimmpt  46781  smfinflem  46788  smflimsuplem7  46797  smflimsuplem8  46798  smflimsupmpt  46800  smfliminfmpt  46803  fsupdm  46813  finfdm  46817  ich2exprop  47445  ichnreuop  47446  2arymaptfo  48616