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  3539  mob  3679  nffrecs  8223  infpssrlem4  10219  axcc3  10351  axdc3lem4  10366  axdc4lem  10368  axacndlem4  10523  axacndlem5  10524  axacnd  10525  dedekind  11297  dedekindle  11298  nfcprod1  15833  nfcprod  15834  fprodle  15921  mreexexd  17572  gsumsnf  19850  gsummatr01lem4  22561  iunconn  23331  hasheuni  34054  measvunilem  34181  measvunilem0  34182  measvuni  34183  volfiniune  34199  bnj919  34736  bnj1379  34799  bnj571  34875  bnj607  34885  bnj873  34893  bnj964  34912  bnj981  34919  bnj1123  34955  bnj1128  34959  bnj1204  34981  bnj1279  34987  bnj1388  35002  bnj1398  35003  bnj1417  35010  bnj1444  35012  bnj1445  35013  bnj1449  35017  bnj1489  35025  bnj1518  35033  bnj1525  35038  dfon2lem1  35759  dfon2lem3  35761  isbasisrelowllem1  37331  isbasisrelowllem2  37332  poimirlem27  37629  upixp  37711  sdclem1  37725  pmapglbx  39751  cdlemefr29exN  40384  gneispace  44110  tratrb  44513  rfcnnnub  45017  uzwo4  45034  suprnmpt  45155  choicefi  45181  iunmapsn  45198  infxr  45350  rexabslelem  45401  fsumiunss  45560  fmuldfeqlem1  45567  fmuldfeq  45568  fmul01lt1  45571  mullimc  45601  mullimcf  45608  limsupre  45626  addlimc  45633  0ellimcdiv  45634  fnlimfvre  45659  climinf2mpt  45699  climinfmpt  45700  limsupmnfuzlem  45711  dvmptfprodlem  45929  dvmptfprod  45930  dvnprodlem1  45931  iblspltprt  45958  stoweidlem16  46001  stoweidlem17  46002  stoweidlem19  46004  stoweidlem20  46005  stoweidlem22  46007  stoweidlem26  46011  stoweidlem28  46013  stoweidlem31  46016  stoweidlem34  46019  stoweidlem35  46020  stoweidlem48  46033  stoweidlem52  46037  stoweidlem53  46038  stoweidlem56  46041  stoweidlem57  46042  stoweidlem60  46045  fourierdlem73  46164  fourierdlem77  46168  fourierdlem83  46174  fourierdlem87  46178  etransclem32  46251  sge0pnffigt  46381  sge0iunmptlemre  46400  sge0iunmpt  46403  meaiininc2  46473  opnvonmbllem2  46618  issmfle  46730  issmfgt  46741  issmfge  46755  smflimlem2  46757  smflimmpt  46795  smfinflem  46802  smflimsuplem7  46811  smflimsuplem8  46812  smflimsupmpt  46814  smfliminfmpt  46817  fsupdm  46827  finfdm  46831  ich2exprop  47459  ichnreuop  47460  2arymaptfo  48643