Theorem nfan 1618

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

Step	Hyp	Ref	Expression
1		nfan.1	. 2 |- F/ x ph
2		nfan.2	. . 3 |- F/ x ps
3	2	a1i 9	. 2 |- ( ph -> F/ x ps )
4	1, 3	nfan1 1617	1 |- F/ x ( ph /\ ps )

This proof depends on syntax axioms:   /\ wa 104   F/wnf 1513

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563

This proof depends on definitions:  df-bi 117  df-nf 1514

This theorem is used by:  nf3an  1619  cbvex2  1978  nfsbxyt  2003  nfsbv  2007  sbcomxyyz  2032  nfsb4t  2074  clelab  2366  nfel  2401  2ralbida  2571  r19.29an  2693  reean  2720  nfrabw  2733  cbvrmow  2735  cbvrexfw  2776  cbvrexf  2778  cbvreu  2784  cbvrab  2819  ceqsex2  2863  vtocl2gaf  2890  rspce  2924  eqvincf  2951  elrabf  2980  elrab3t  2981  rexab2  2992  morex  3010  reu2  3014  rmo3f  3023  sbc2iegf  3122  reu8nf  3133  rmo2ilem  3142  rmo3  3144  csbiebt  3187  csbie2t  3196  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  rabsnifsb  3777  nfopd  3921  eluniab  3947  dfnfc2  3953  nfdisjv  4118  disjiun  4125  nfopab  4199  cbvopab  4202  cbvopab1  4204  cbvopab2  4205  cbvopab1s  4206  mpteq12f  4211  nfmpt  4223  cbvmptf  4225  cbvmpt  4226  repizf2  4299  nfpo  4446  nfso  4447  nfwe  4500  onintonm  4664  peano2  4742  nfxp  4801  opeliunxp  4830  nfco  4945  elrnmpt1  5033  nfimad  5135  iota2  5367  dffun4f  5393  nffun  5400  imadif  5461  funimaexglem  5464  nffn  5477  nff  5530  nff1  5596  nffo  5614  nff1o  5637  fun11iun  5660  nffvd  5707  fv3  5718  fmptco  5874  nfiso  6012  cbvriota  6050  riota2df  6060  riota5f  6065  nfoprab  6140  mpoeq123  6147  nfmpo  6157  cbvoprab1  6160  cbvoprab2  6161  cbvoprab12  6162  cbvoprab3  6164  cbvmpox  6166  ovmpodxf  6214  elovmporab  6289  elovmporab1w  6290  opabex3d  6350  opabex3  6351  funimass4f  6359  uchoice  6371  dfoprab4f  6427  fmpox  6436  spc2ed  6469  cnvoprab  6470  f1od2  6471  opeliunxp2f  6509  nfrecs  6578  tfri3  6638  nffrec  6667  erovlem  6901  nfixpxy  6999  nfixp1  7000  modom  7108  xpf1o  7144  nneneq  7158  ac6sfi  7202  opabfi  7247  nfsup  7332  exmidomni  7482  fodjuomnilemdc  7484  ismkvnex  7495  mkvprop  7498  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  cc3  7634  caucvgsrlemgt1  8162  suplocsrlem  8175  axpre-suploclemres  8268  supinfneg  9995  infsupneg  9996  zsupcllemstep  10662  nninfinf  10880  reuccatpfxs1  11519  fimaxre2  11993  nfsum1  12122  nfsum  12123  fsumsplitf  12175  fsum2dlemstep  12201  fsum00  12229  nfcprod1  12321  nfcprod  12322  prodeq2  12324  fprod2dlemstep  12389  fprodsplitf  12399  fprodsplit1f  12401  fprodap0f  12403  fprodle  12407  bezoutlemmain  12775  bezoutlemzz  12779  bezout  12788  exmidunben  13317  ctiunctlemfo  13330  ctiunct  13331  mulcncf  15709  ellimc3apf  15761  limccnp2cntop  15778  bdsepnft  16913  bdsepnfALT  16915  bj-findis  17005  strcollnft  17010  strcollnfALT  17012  pw1nct  17033  isomninnlem  17079  trirec0  17093  iswomninnlem  17099  ismkvnnlem  17102  nfals  17144  nfrals  17145  nfalseu  17175  nfralseu  17176