Theorem nf3an 1907

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

Syntax hints:   ∧ wa 395   ∧ w3a 1085  Ⅎwnf 1789

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-ex 1786  df-nf 1790

This theorem is referenced by:  hb3an  2301  vtocl3gaf  3514  mob  3655  nffrecs  8083  nfwrecsOLD  8117  infpssrlem4  10046  axcc3  10178  axdc3lem4  10193  axdc4lem  10195  axacndlem4  10350  axacndlem5  10351  axacnd  10352  dedekind  11121  dedekindle  11122  nfcprod1  15601  nfcprod  15602  fprodle  15687  mreexexd  17338  gsumsnf  19535  gsummatr01lem4  21788  iunconn  22560  hasheuni  32032  measvunilem  32159  measvunilem0  32160  measvuni  32161  volfiniune  32177  bnj919  32726  bnj1379  32789  bnj571  32865  bnj607  32875  bnj873  32883  bnj964  32902  bnj981  32909  bnj1123  32945  bnj1128  32949  bnj1204  32971  bnj1279  32977  bnj1388  32992  bnj1398  32993  bnj1417  33000  bnj1444  33002  bnj1445  33003  bnj1449  33007  bnj1489  33015  bnj1518  33023  bnj1525  33028  dfon2lem1  33738  dfon2lem3  33740  isbasisrelowllem1  35505  isbasisrelowllem2  35506  poimirlem27  35783  upixp  35866  sdclem1  35880  pmapglbx  37762  cdlemefr29exN  38395  gneispace  41697  tratrb  42109  rfcnnnub  42532  uzwo4  42554  suprnmpt  42663  choicefi  42693  iunmapsn  42710  infxr  42860  rexabslelem  42912  fsumiunss  43070  fmuldfeqlem1  43077  fmuldfeq  43078  fmul01lt1  43081  mullimc  43111  mullimcf  43118  limsupre  43136  addlimc  43143  0ellimcdiv  43144  fnlimfvre  43169  climinf2mpt  43209  climinfmpt  43210  limsupmnfuzlem  43221  dvmptfprodlem  43439  dvmptfprod  43440  dvnprodlem1  43441  iblspltprt  43468  stoweidlem16  43511  stoweidlem17  43512  stoweidlem19  43514  stoweidlem20  43515  stoweidlem22  43517  stoweidlem26  43521  stoweidlem28  43523  stoweidlem31  43526  stoweidlem34  43529  stoweidlem35  43530  stoweidlem48  43543  stoweidlem52  43547  stoweidlem53  43548  stoweidlem56  43551  stoweidlem57  43552  stoweidlem60  43555  fourierdlem73  43674  fourierdlem77  43678  fourierdlem83  43684  fourierdlem87  43688  etransclem32  43761  sge0pnffigt  43888  sge0iunmptlemre  43907  sge0iunmpt  43910  meaiininc2  43980  opnvonmbllem2  44125  issmfle  44232  issmfgt  44243  issmfge  44256  smflimlem2  44258  smflimmpt  44294  smfinflem  44301  smflimsuplem7  44310  smflimsuplem8  44311  smflimsupmpt  44313  smfliminfmpt  44316  ich2exprop  44875  ichnreuop  44876  2arymaptfo  45952