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

Theorem nf3an 1930
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 975 . 2
2 nfan.1 . . . 4
3 nfan.2 . . . 4
42, 3nfan 1928 . . 3
5 nfan.3 . . 3
64, 5nfan 1928 . 2
71, 6nfxfr 1645 1
Colors of variables: wff setvar class
Syntax hints:  /\wa 369  /\w3a 973  F/wnf 1616
This theorem is referenced by:  hb3an  1932  vtocl3gaf  3176  mob  3281  reusv6OLD  4663  infpssrlem4  8707  axcc3  8839  axdc3lem4  8854  axdc4lem  8856  axacndlem4  9009  axacndlem5  9010  axacnd  9011  dedekind  9765  dedekindle  9766  nfcprod1  13717  nfcprod  13718  mreexexd  15045  gsumsnf  16980  gsummatr01lem4  19160  iuncon  19929  hasheuni  28091  measvunilem  28183  measvunilem0  28184  measvuni  28185  volfiniune  28202  dfon2lem1  29215  dfon2lem3  29217  nfwrecs  29338  upixp  30220  sdclem1  30236  rfcnnnub  31411  suprnmpt  31451  fmuldfeqlem1  31576  fmuldfeq  31577  fmul01lt1  31580  infrglb  31584  fprodle  31604  mullimc  31622  mullimcf  31629  limsupre  31647  addlimc  31654  0ellimcdiv  31655  dvmptfprodlem  31741  dvmptfprod  31742  dvnprodlem1  31743  iblspltprt  31772  stoweidlem16  31798  stoweidlem17  31799  stoweidlem19  31801  stoweidlem20  31802  stoweidlem22  31804  stoweidlem26  31808  stoweidlem28  31810  stoweidlem31  31813  stoweidlem34  31816  stoweidlem35  31817  stoweidlem48  31830  stoweidlem52  31834  stoweidlem53  31835  stoweidlem56  31838  stoweidlem57  31839  stoweidlem60  31842  fourierdlem73  31962  fourierdlem77  31966  fourierdlem83  31972  fourierdlem87  31976  etransclem32  32049  tratrb  33307  bnj919  33825  bnj1379  33889  bnj571  33964  bnj607  33974  bnj873  33982  bnj964  34001  bnj981  34008  bnj1123  34042  bnj1128  34046  bnj1204  34068  bnj1279  34074  bnj1388  34089  bnj1398  34090  bnj1417  34097  bnj1444  34099  bnj1445  34100  bnj1449  34104  bnj1489  34112  bnj1518  34120  bnj1525  34125  pmapglbx  35493  cdlemefr29exN  36128
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-ex 1613  df-nf 1617
  Copyright terms: Public domain W3C validator