Theorem nf3an 1905

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

Syntax hints:   ∧ wa 397   ∧ w3a 1088  Ⅎwnf 1786

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-ex 1783  df-nf 1787

This theorem is referenced by:  hb3an  2298  vtocl3gaf  3569  mob  3714  nffrecs  8268  nfwrecsOLD  8302  infpssrlem4  10301  axcc3  10433  axdc3lem4  10448  axdc4lem  10450  axacndlem4  10605  axacndlem5  10606  axacnd  10607  dedekind  11377  dedekindle  11378  nfcprod1  15854  nfcprod  15855  fprodle  15940  mreexexd  17592  gsumsnf  19821  gsummatr01lem4  22160  iunconn  22932  hasheuni  33114  measvunilem  33241  measvunilem0  33242  measvuni  33243  volfiniune  33259  bnj919  33809  bnj1379  33872  bnj571  33948  bnj607  33958  bnj873  33966  bnj964  33985  bnj981  33992  bnj1123  34028  bnj1128  34032  bnj1204  34054  bnj1279  34060  bnj1388  34075  bnj1398  34076  bnj1417  34083  bnj1444  34085  bnj1445  34086  bnj1449  34090  bnj1489  34098  bnj1518  34106  bnj1525  34111  dfon2lem1  34786  dfon2lem3  34788  isbasisrelowllem1  36284  isbasisrelowllem2  36285  poimirlem27  36563  upixp  36645  sdclem1  36659  pmapglbx  38688  cdlemefr29exN  39321  gneispace  42933  tratrb  43345  rfcnnnub  43768  uzwo4  43788  suprnmpt  43918  choicefi  43947  iunmapsn  43964  infxr  44125  rexabslelem  44176  fsumiunss  44339  fmuldfeqlem1  44346  fmuldfeq  44347  fmul01lt1  44350  mullimc  44380  mullimcf  44387  limsupre  44405  addlimc  44412  0ellimcdiv  44413  fnlimfvre  44438  climinf2mpt  44478  climinfmpt  44479  limsupmnfuzlem  44490  dvmptfprodlem  44708  dvmptfprod  44709  dvnprodlem1  44710  iblspltprt  44737  stoweidlem16  44780  stoweidlem17  44781  stoweidlem19  44783  stoweidlem20  44784  stoweidlem22  44786  stoweidlem26  44790  stoweidlem28  44792  stoweidlem31  44795  stoweidlem34  44798  stoweidlem35  44799  stoweidlem48  44812  stoweidlem52  44816  stoweidlem53  44817  stoweidlem56  44820  stoweidlem57  44821  stoweidlem60  44824  fourierdlem73  44943  fourierdlem77  44947  fourierdlem83  44953  fourierdlem87  44957  etransclem32  45030  sge0pnffigt  45160  sge0iunmptlemre  45179  sge0iunmpt  45182  meaiininc2  45252  opnvonmbllem2  45397  issmfle  45509  issmfgt  45520  issmfge  45534  smflimlem2  45536  smflimmpt  45574  smfinflem  45581  smflimsuplem7  45590  smflimsuplem8  45591  smflimsupmpt  45593  smfliminfmpt  45596  fsupdm  45606  finfdm  45610  ich2exprop  46187  ichnreuop  46188  2arymaptfo  47388