Theorem nf3an 1903

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

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

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-nf 1786

This theorem is referenced by:  hb3an  2308  vtocl3gafOLD  3539  mob  3677  nffrecs  8235  infpssrlem4  10228  axcc3  10360  axdc3lem4  10375  axdc4lem  10377  axacndlem4  10533  axacndlem5  10534  axacnd  10535  dedekind  11308  dedekindle  11309  nfcprod1  15843  nfcprod  15844  fprodle  15931  mreexexd  17583  gsumsnf  19894  gsummatr01lem4  22614  iunconn  23384  hasheuni  34262  measvunilem  34389  measvunilem0  34390  measvuni  34391  volfiniune  34407  bnj919  34943  bnj1379  35005  bnj571  35081  bnj607  35091  bnj873  35099  bnj964  35118  bnj981  35125  bnj1123  35161  bnj1128  35165  bnj1204  35187  bnj1279  35193  bnj1388  35208  bnj1398  35209  bnj1417  35216  bnj1444  35218  bnj1445  35219  bnj1449  35223  bnj1489  35231  bnj1518  35239  bnj1525  35244  dfon2lem1  35994  dfon2lem3  35996  isbasisrelowllem1  37607  isbasisrelowllem2  37608  poimirlem27  37895  upixp  37977  sdclem1  37991  pmapglbx  40142  cdlemefr29exN  40775  gneispace  44487  tratrb  44889  rfcnnnub  45393  uzwo4  45410  suprnmpt  45530  choicefi  45555  iunmapsn  45572  infxr  45722  rexabslelem  45773  fsumiunss  45932  fmuldfeqlem1  45939  fmuldfeq  45940  fmul01lt1  45943  mullimc  45973  mullimcf  45980  limsupre  45996  addlimc  46003  0ellimcdiv  46004  fnlimfvre  46029  climinf2mpt  46069  climinfmpt  46070  limsupmnfuzlem  46081  dvmptfprodlem  46299  dvmptfprod  46300  dvnprodlem1  46301  iblspltprt  46328  stoweidlem16  46371  stoweidlem17  46372  stoweidlem19  46374  stoweidlem20  46375  stoweidlem22  46377  stoweidlem26  46381  stoweidlem28  46383  stoweidlem31  46386  stoweidlem34  46389  stoweidlem35  46390  stoweidlem48  46403  stoweidlem52  46407  stoweidlem53  46408  stoweidlem56  46411  stoweidlem57  46412  stoweidlem60  46415  fourierdlem73  46534  fourierdlem77  46538  fourierdlem83  46544  fourierdlem87  46548  etransclem32  46621  sge0pnffigt  46751  sge0iunmptlemre  46770  sge0iunmpt  46773  meaiininc2  46843  opnvonmbllem2  46988  issmfle  47100  issmfgt  47111  issmfge  47125  smflimlem2  47127  smflimmpt  47165  smfinflem  47172  smflimsuplem7  47181  smflimsuplem8  47182  smflimsupmpt  47184  smfliminfmpt  47187  fsupdm  47197  finfdm  47201  ich2exprop  47828  ichnreuop  47829  2arymaptfo  49011