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

Theorem nfan 1861
Description: If  x is not free in  ph and  ps, it is not free in  ( ph  /\  ps ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.)
Hypotheses
Ref Expression
nfan.1  |-  F/ x ph
nfan.2  |-  F/ x ps
Assertion
Ref Expression
nfan  |-  F/ x
( ph  /\  ps )

Proof of Theorem nfan
StepHypRef Expression
1 nfan.1 . 2  |-  F/ x ph
2 nfan.2 . . 3  |-  F/ x ps
32a1i 11 . 2  |-  ( ph  ->  F/ x ps )
41, 3nfan1 1860 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369   F/wnf 1589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590
This theorem is referenced by:  nfnan  1862  nf3an  1863  hban  1864  cbvex2OLD  1977  nfeqf  1993  nfald2  2023  nfsb4t  2080  2ax6elem  2157  nfeud2OLD  2280  mopickOLDOLD  2341  eupicka  2343  mopick2  2348  2mo  2360  2moOLD  2361  2eu6OLD  2372  axbnd  2422  clelab  2571  clelabOLD  2572  nfelOLD  2602  nfabd2  2609  2ralbida  2775  ralcom2  2906  reean  2908  cbvreu  2966  cbvrab  2991  ceqsex2  3031  vtocl2gaf  3058  rspce  3089  eqvincf  3108  elrabf  3136  elrab3t  3137  rexab2  3147  morex  3164  reu2  3168  sbc2iegf  3282  rmo2  3304  rmo3  3306  csbiebt  3329  csbie2t  3337  cbvreucsf  3342  cbvrabcsf  3343  rabsnifsb  3964  nfop  4096  nfopd  4097  eluniab  4123  dfnfc2  4130  nfopab  4378  cbvopab  4381  cbvopab1  4383  cbvopab2  4384  cbvopab1s  4385  mpteq12f  4389  nfmpt  4401  cbvmpt  4403  axrep3  4427  axrep4  4428  axrep5  4429  reusv2lem2  4515  reusv2lem3  4516  reusv6OLD  4524  nfpo  4667  nfso  4668  nffr  4715  nfwe  4717  nfxp  4887  opeliunxp  4911  nfco  5026  elrnmpt1  5109  nfimad  5199  iota2  5428  nffun  5461  imadif  5514  nffn  5528  nff  5576  nff1  5625  nffo  5640  nff1o  5660  nffvd  5721  fv3  5724  fmptco  5897  nfiso  6036  nfriotad  6081  cbvriota  6083  riota2df  6094  riota5f  6098  nfoprab  6159  mpt2eq123  6166  nfmpt2  6176  cbvoprab1  6179  cbvoprab2  6180  cbvoprab12  6181  cbvoprab3  6183  cbvmpt2x  6185  ovmpt2dxf  6237  onminex  6439  peano5  6520  fun11iun  6558  opabex3d  6576  opabex3  6577  dfoprab4f  6653  fmpt2x  6661  nfrecs  6855  tfr3  6879  tz7.49  6921  erovlem  7217  nfixp  7303  nfixp1  7304  xpf1o  7494  nneneq  7515  ac6sfi  7577  nfoi  7749  wdom2d  7816  infpssrlem4  8496  hsmexlem2  8617  hsmexlem4  8619  domtriomlem  8632  axdc3lem2  8641  axdc4lem  8645  zorn2lem4  8689  zorn2lem5  8690  konigthlem  8753  axextnd  8776  axrepndlem2  8778  axrepnd  8779  axunnd  8781  axpowndlem2  8783  axpowndlem2OLD  8784  axpowndlem4  8787  axpownd  8788  axregndlem2  8790  axregnd  8791  axregndOLD  8792  axinfndlem1  8793  axinfnd  8794  zfcndrep  8802  zfcndinf  8806  dedekind  9554  dedekindle  9555  nfsum1  13188  nfsum  13189  fsum2dlem  13258  fsum00  13282  mreexexd  14607  acsmapd  15369  gsummptshft  16451  gsum2d2lem  16487  dprd2d2  16565  gsummatr01lem4  18486  neiptopnei  18758  neiptopreu  18759  neitr  18806  iunconlem  19053  iuncon  19054  ptcnplem  19216  ptcnp  19217  xkocnv  19409  isfildlem  19452  utopsnneiplem  19844  isucn2  19876  cfilucfilOLD  20166  cfilucfil  20167  restmetu  20184  ovolfiniun  21006  ovoliunlem3  21009  ovoliunnul  21012  volfiniun  21050  itg2splitlem  21248  itg2split  21249  isibl2  21266  nfitg  21274  cbvitg  21275  limciun  21391  colline  23074  f1otrg  23139  chirred  25821  spc2ed  25879  mo5f  25890  rmo3f  25901  rmo4fOLD  25902  cbvdisjf  25939  disjabrex  25948  disjabrexf  25949  funimass4f  25973  cbvmptf  25993  fmptcof2  26001  fcomptf  26002  funcnv4mpt  26011  cnvoprab  26045  f1od2  26046  fpwrelmap  26055  xrofsup  26077  nn0min  26112  isarchi3  26226  isarchiofld  26307  ordtconlem1  26376  esumcl  26508  gsumesum  26532  esumlub  26533  esumcst  26536  esumfzf  26540  esumfsup  26541  hasheuni  26556  esumcvg  26557  measvunilem  26648  measvunilem0  26649  measvuni  26650  measinblem  26656  voliune  26667  volfiniune  26668  volmeas  26669  oms0  26732  eulerpartlemgvv  26781  dstrvprob  26876  cvmcov  27174  iota5f  27403  nfcprod1  27445  nfcprod  27446  fprod2dlem  27513  axextdist  27635  axext4dist  27636  trpredmintr  27717  nfwrecs  27741  wfrlem4  27749  nfwlim  27781  frrlem4  27793  wl-cbvalnaed  28387  wl-2sb6d  28410  wl-sbalnae  28414  wl-ax11-lem3  28429  heicant  28452  mbfposadd  28465  ftc1anclem5  28497  finminlem  28539  indexdom  28654  filbcmb  28660  sdclem2  28664  sdclem1  28665  fdc1  28668  mzpsubmpt  29105  mzpexpmpt  29107  eq0rabdioph  29141  eqrabdioph  29142  setindtr  29399  elunif  29764  rspcegf  29771  fnchoice  29777  refsumcn  29778  rfcnnnub  29784  fmul01  29787  fmuldfeqlem1  29789  fmuldfeq  29790  fmul01lt1lem1  29791  fmul01lt1lem2  29792  infrglb  29797  climmulf  29803  climexp  29804  climsuse  29807  climrecf  29808  climinff  29810  stoweidlem3  29824  stoweidlem26  29847  stoweidlem27  29848  stoweidlem29  29850  stoweidlem31  29852  stoweidlem34  29855  stoweidlem35  29856  stoweidlem36  29857  stoweidlem39  29860  stoweidlem42  29863  stoweidlem43  29864  stoweidlem44  29865  stoweidlem46  29867  stoweidlem48  29869  stoweidlem49  29870  stoweidlem51  29872  stoweidlem52  29873  stoweidlem53  29874  stoweidlem54  29875  stoweidlem55  29876  stoweidlem56  29877  stoweidlem57  29878  stoweidlem58  29879  stoweidlem59  29880  stoweidlem60  29881  stoweidlem61  29882  stoweidlem62  29883  stoweid  29884  wallispilem3  29888  stirlinglem13  29907  stirling  29910  nfdfat  30062  oprabv  30183  elovmpt2rab  30184  elovmpt2rab1  30185  rabasiun  30256  opeliun2xp  30746  cbvmpt2x2  30753  ovmpt2rdxf  30756  fsuppmapnn0fiublem  30828  fsuppmapnn0fiub  30829  fsuppmapnn0fiubex  30830  gsummoncoe1  30876  cnstpmatmcllem  31070  iunconlem2  31767  bnj919  31856  bnj1146  31881  bnj1379  31920  bnj849  32014  bnj916  32022  bnj964  32032  bnj1014  32049  bnj1123  32073  bnj1228  32098  bnj1307  32110  bnj1321  32114  bnj1398  32121  bnj1408  32123  bnj1444  32130  bnj1445  32131  bnj1446  32132  bnj1449  32135  bnj1467  32141  bnj1463  32142  bnj1489  32143  bnj1491  32144  bnj1312  32145  bnj1525  32156  bj-axrep3  32407  bj-axrep4  32408  bj-axrep5  32409  riotasv2d  32704  riotasv2s  32705  glbconxN  33118  pmapglb2xN  33512  cdlemefs32sn1aw  34154
  Copyright terms: Public domain W3C validator