MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nf3an Structured version   Visualization version   GIF version

Theorem nf3an 1818
Description: If 𝑥 is not free in 𝜑, 𝜓, and 𝜒, 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
StepHypRef Expression
1 df-3an 1032 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 nfan.1 . . . 4 𝑥𝜑
3 nfan.2 . . . 4 𝑥𝜓
42, 3nfan 1815 . . 3 𝑥(𝜑𝜓)
5 nfan.3 . . 3 𝑥𝜒
64, 5nfan 1815 . 2 𝑥((𝜑𝜓) ∧ 𝜒)
71, 6nfxfr 1770 1 𝑥(𝜑𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  wa 382  w3a 1030  wnf 1698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700
This theorem is referenced by:  hb3an  2113  vtocl3gaf  3247  mob  3354  nfwrecs  7274  infpssrlem4  8989  axcc3  9121  axdc3lem4  9136  axdc4lem  9138  axacndlem4  9289  axacndlem5  9290  axacnd  9291  dedekind  10052  dedekindle  10053  nfcprod1  14428  nfcprod  14429  fprodle  14515  mreexexd  16080  mreexexdOLD  16081  gsumsnf  18125  gsummatr01lem4  20231  iuncon  20989  hasheuni  29308  measvunilem  29436  measvunilem0  29437  measvuni  29438  volfiniune  29454  bnj919  29925  bnj1379  29989  bnj571  30064  bnj607  30074  bnj873  30082  bnj964  30101  bnj981  30108  bnj1123  30142  bnj1128  30146  bnj1204  30168  bnj1279  30174  bnj1388  30189  bnj1398  30190  bnj1417  30197  bnj1444  30199  bnj1445  30200  bnj1449  30204  bnj1489  30212  bnj1518  30220  bnj1525  30225  dfon2lem1  30766  dfon2lem3  30768  isbasisrelowllem1  32203  isbasisrelowllem2  32204  poimirlem27  32430  upixp  32518  sdclem1  32533  pmapglbx  33897  cdlemefr29exN  34532  gneispace  37276  tratrb  37591  rfcnnnub  38042  uzwo4  38070  suprnmpt  38174  wessf1ornlem  38190  choicefi  38211  iunmapsn  38228  infxr  38348  fsumiunss  38466  fmuldfeqlem1  38473  fmuldfeq  38474  fmul01lt1  38477  mullimc  38507  mullimcf  38514  limsupre  38532  addlimc  38539  0ellimcdiv  38540  fnlimfvre  38565  dvmptfprodlem  38658  dvmptfprod  38659  dvnprodlem1  38660  iblspltprt  38689  stoweidlem16  38733  stoweidlem17  38734  stoweidlem19  38736  stoweidlem20  38737  stoweidlem22  38739  stoweidlem26  38743  stoweidlem28  38745  stoweidlem31  38748  stoweidlem34  38751  stoweidlem35  38752  stoweidlem48  38765  stoweidlem52  38769  stoweidlem53  38770  stoweidlem56  38773  stoweidlem57  38774  stoweidlem60  38777  fourierdlem73  38896  fourierdlem77  38900  fourierdlem83  38906  fourierdlem87  38910  etransclem32  38983  sge0pnffigt  39113  sge0iunmptlemre  39132  sge0iunmpt  39135  meaiininc2  39202  opnvonmbllem2  39347  issmfle  39456  issmfgt  39467  issmfge  39480  smflimlem2  39482
  Copyright terms: Public domain W3C validator