Theorem nf3an 1897

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

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

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-ex 1775  df-nf 1779

This theorem is referenced by:  hb3an  2291  vtocl3gaf  3565  mob  3711  nffrecs  8282  nfwrecsOLD  8316  infpssrlem4  10323  axcc3  10455  axdc3lem4  10470  axdc4lem  10472  axacndlem4  10627  axacndlem5  10628  axacnd  10629  dedekind  11401  dedekindle  11402  nfcprod1  15880  nfcprod  15881  fprodle  15966  mreexexd  17621  gsumsnf  19901  gsummatr01lem4  22553  iunconn  23325  hasheuni  33698  measvunilem  33825  measvunilem0  33826  measvuni  33827  volfiniune  33843  bnj919  34392  bnj1379  34455  bnj571  34531  bnj607  34541  bnj873  34549  bnj964  34568  bnj981  34575  bnj1123  34611  bnj1128  34615  bnj1204  34637  bnj1279  34643  bnj1388  34658  bnj1398  34659  bnj1417  34666  bnj1444  34668  bnj1445  34669  bnj1449  34673  bnj1489  34681  bnj1518  34689  bnj1525  34694  dfon2lem1  35373  dfon2lem3  35375  isbasisrelowllem1  36828  isbasisrelowllem2  36829  poimirlem27  37114  upixp  37196  sdclem1  37210  pmapglbx  39236  cdlemefr29exN  39869  gneispace  43558  tratrb  43969  rfcnnnub  44392  uzwo4  44411  suprnmpt  44541  choicefi  44567  iunmapsn  44584  infxr  44743  rexabslelem  44794  fsumiunss  44957  fmuldfeqlem1  44964  fmuldfeq  44965  fmul01lt1  44968  mullimc  44998  mullimcf  45005  limsupre  45023  addlimc  45030  0ellimcdiv  45031  fnlimfvre  45056  climinf2mpt  45096  climinfmpt  45097  limsupmnfuzlem  45108  dvmptfprodlem  45326  dvmptfprod  45327  dvnprodlem1  45328  iblspltprt  45355  stoweidlem16  45398  stoweidlem17  45399  stoweidlem19  45401  stoweidlem20  45402  stoweidlem22  45404  stoweidlem26  45408  stoweidlem28  45410  stoweidlem31  45413  stoweidlem34  45416  stoweidlem35  45417  stoweidlem48  45430  stoweidlem52  45434  stoweidlem53  45435  stoweidlem56  45438  stoweidlem57  45439  stoweidlem60  45442  fourierdlem73  45561  fourierdlem77  45565  fourierdlem83  45571  fourierdlem87  45575  etransclem32  45648  sge0pnffigt  45778  sge0iunmptlemre  45797  sge0iunmpt  45800  meaiininc2  45870  opnvonmbllem2  46015  issmfle  46127  issmfgt  46138  issmfge  46152  smflimlem2  46154  smflimmpt  46192  smfinflem  46199  smflimsuplem7  46208  smflimsuplem8  46209  smflimsupmpt  46211  smfliminfmpt  46214  fsupdm  46224  finfdm  46228  ich2exprop  46805  ichnreuop  46806  2arymaptfo  47721

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »