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  4200  cbvopab  4203  cbvopab1  4205  cbvopab2  4206  cbvopab1s  4207  mpteq12f  4212  nfmpt  4225  cbvmptf  4227  cbvmpt  4228  repizf2  4301  nfpo  4448  nfso  4449  nfwe  4502  onintonm  4666  peano2  4744  nfxp  4803  opeliunxp  4832  nfco  4947  elrnmpt1  5035  nfimad  5138  iota2  5370  dffun4f  5396  nffun  5403  imadif  5464  funimaexglem  5467  nffn  5480  nff  5533  nff1  5599  nffo  5617  nff1o  5640  fun11iun  5663  nffvd  5710  fv3  5721  fmptco  5877  nfiso  6015  cbvriota  6053  riota2df  6063  riota5f  6068  nfoprab  6143  mpoeq123  6150  nfmpo  6160  cbvoprab1  6163  cbvoprab2  6164  cbvoprab12  6165  cbvoprab3  6167  cbvmpox  6169  ovmpodxf  6217  elovmporab  6292  elovmporab1w  6293  opabex3d  6354  opabex3  6355  funimass4f  6363  uchoice  6375  dfoprab4f  6431  fmpox  6440  spc2ed  6473  cnvoprab  6474  f1od2  6475  opeliunxp2f  6514  nfrecs  6583  tfri3  6643  nffrec  6672  erovlem  6906  nfixpxy  7005  nfixp1  7006  modom  7114  xpf1o  7150  nneneq  7164  ac6sfi  7208  opabfi  7253  nfsup  7338  exmidomni  7488  fodjuomnilemdc  7490  ismkvnex  7501  mkvprop  7504  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  cc3  7640  caucvgsrlemgt1  8168  suplocsrlem  8181  axpre-suploclemres  8274  supinfneg  10010  infsupneg  10011  zsupcllemstep  10678  nninfinf  10900  reuccatpfxs1  11540  fimaxre2  12015  nfsum1  12146  nfsum  12147  fsumsplitf  12199  fsum2dlemstep  12225  fsum00  12253  nfcprod1  12345  nfcprod  12346  prodeq2  12348  fprod2dlemstep  12413  fprodsplitf  12423  fprodsplit1f  12425  fprodap0f  12427  fprodle  12431  bezoutlemmain  12799  bezoutlemzz  12803  bezout  12812  exmidunben  13374  ctiunctlemfo  13387  ctiunct  13388  gsumsnfdcmn  14256  mulcncf  15851  ellimc3apf  15903  limccnp2cntop  15920  bdsepnft  17135  bdsepnfALT  17137  bj-findis  17227  strcollnft  17232  strcollnfALT  17234  pw1nct  17255  isomninnlem  17302  trirec0  17317  iswomninnlem  17323  ismkvnnlem  17326  nfals  17368  nfrals  17369  nfalseu  17399  nfralseu  17400