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 )

Syntax hints:   /\ wa 104   F/wnf 1513

This theorem was proved from 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 theorem depends on definitions:  df-bi 117  df-nf 1514

This theorem is referenced 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  3773  nfopd  3916  eluniab  3942  dfnfc2  3948  nfdisjv  4113  disjiun  4120  nfopab  4194  cbvopab  4197  cbvopab1  4199  cbvopab2  4200  cbvopab1s  4201  mpteq12f  4206  nfmpt  4218  cbvmptf  4220  cbvmpt  4221  repizf2  4294  nfpo  4441  nfso  4442  nfwe  4495  onintonm  4659  peano2  4737  nfxp  4796  opeliunxp  4825  nfco  4940  elrnmpt1  5028  nfimad  5130  iota2  5362  dffun4f  5388  nffun  5395  imadif  5456  funimaexglem  5459  nffn  5472  nff  5525  nff1  5591  nffo  5609  nff1o  5632  fun11iun  5655  nffvd  5702  fv3  5713  fmptco  5865  nfiso  6002  cbvriota  6040  riota2df  6050  riota5f  6055  nfoprab  6130  mpoeq123  6137  nfmpo  6147  cbvoprab1  6150  cbvoprab2  6151  cbvoprab12  6152  cbvoprab3  6154  cbvmpox  6156  ovmpodxf  6204  elovmporab  6279  elovmporab1w  6280  opabex3d  6340  opabex3  6341  funimass4f  6349  uchoice  6361  dfoprab4f  6417  fmpox  6426  spc2ed  6459  cnvoprab  6460  f1od2  6461  opeliunxp2f  6499  nfrecs  6568  tfri3  6628  nffrec  6657  erovlem  6891  nfixpxy  6989  nfixp1  6990  modom  7098  xpf1o  7134  nneneq  7148  ac6sfi  7192  opabfi  7237  nfsup  7322  exmidomni  7472  fodjuomnilemdc  7474  ismkvnex  7485  mkvprop  7488  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  cc3  7624  caucvgsrlemgt1  8152  suplocsrlem  8165  axpre-suploclemres  8258  supinfneg  9974  infsupneg  9975  zsupcllemstep  10640  nninfinf  10858  reuccatpfxs1  11497  fimaxre2  11971  nfsum1  12100  nfsum  12101  fsumsplitf  12153  fsum2dlemstep  12179  fsum00  12207  nfcprod1  12299  nfcprod  12300  prodeq2  12302  fprod2dlemstep  12367  fprodsplitf  12377  fprodsplit1f  12379  fprodap0f  12381  fprodle  12385  bezoutlemmain  12753  bezoutlemzz  12757  bezout  12766  exmidunben  13295  ctiunctlemfo  13308  ctiunct  13309  mulcncf  15632  ellimc3apf  15684  limccnp2cntop  15701  bdsepnft  16827  bdsepnfALT  16829  bj-findis  16919  strcollnft  16924  strcollnfALT  16926  pw1nct  16947  isomninnlem  16984  trirec0  16998  iswomninnlem  17004  ismkvnnlem  17007