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  3548  mob  3688  nffrecs  8262  infpssrlem4  10259  axcc3  10391  axdc3lem4  10406  axdc4lem  10408  axacndlem4  10563  axacndlem5  10564  axacnd  10565  dedekind  11337  dedekindle  11338  nfcprod1  15874  nfcprod  15875  fprodle  15962  mreexexd  17609  gsumsnf  19883  gsummatr01lem4  22545  iunconn  23315  hasheuni  34075  measvunilem  34202  measvunilem0  34203  measvuni  34204  volfiniune  34220  bnj919  34757  bnj1379  34820  bnj571  34896  bnj607  34906  bnj873  34914  bnj964  34933  bnj981  34940  bnj1123  34976  bnj1128  34980  bnj1204  35002  bnj1279  35008  bnj1388  35023  bnj1398  35024  bnj1417  35031  bnj1444  35033  bnj1445  35034  bnj1449  35038  bnj1489  35046  bnj1518  35054  bnj1525  35059  dfon2lem1  35771  dfon2lem3  35773  isbasisrelowllem1  37343  isbasisrelowllem2  37344  poimirlem27  37641  upixp  37723  sdclem1  37737  pmapglbx  39763  cdlemefr29exN  40396  gneispace  44123  tratrb  44526  rfcnnnub  45030  uzwo4  45047  suprnmpt  45168  choicefi  45194  iunmapsn  45211  infxr  45363  rexabslelem  45414  fsumiunss  45573  fmuldfeqlem1  45580  fmuldfeq  45581  fmul01lt1  45584  mullimc  45614  mullimcf  45621  limsupre  45639  addlimc  45646  0ellimcdiv  45647  fnlimfvre  45672  climinf2mpt  45712  climinfmpt  45713  limsupmnfuzlem  45724  dvmptfprodlem  45942  dvmptfprod  45943  dvnprodlem1  45944  iblspltprt  45971  stoweidlem16  46014  stoweidlem17  46015  stoweidlem19  46017  stoweidlem20  46018  stoweidlem22  46020  stoweidlem26  46024  stoweidlem28  46026  stoweidlem31  46029  stoweidlem34  46032  stoweidlem35  46033  stoweidlem48  46046  stoweidlem52  46050  stoweidlem53  46051  stoweidlem56  46054  stoweidlem57  46055  stoweidlem60  46058  fourierdlem73  46177  fourierdlem77  46181  fourierdlem83  46187  fourierdlem87  46191  etransclem32  46264  sge0pnffigt  46394  sge0iunmptlemre  46413  sge0iunmpt  46416  meaiininc2  46486  opnvonmbllem2  46631  issmfle  46743  issmfgt  46754  issmfge  46768  smflimlem2  46770  smflimmpt  46808  smfinflem  46815  smflimsuplem7  46824  smflimsuplem8  46825  smflimsupmpt  46827  smfliminfmpt  46830  fsupdm  46840  finfdm  46844  ich2exprop  47472  ichnreuop  47473  2arymaptfo  48643