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  6513  nfrecs  6582  tfri3  6642  nffrec  6671  erovlem  6905  nfixpxy  7003  nfixp1  7004  modom  7112  xpf1o  7148  nneneq  7162  ac6sfi  7206  opabfi  7251  nfsup  7338  exmidomni  7488  fodjuomnilemdc  7490  ismkvnex  7501  mkvprop  7504  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  cc3  7640  caucvgsrlemgt1  8168  suplocsrlem  8181  axpre-suploclemres  8274  supinfneg  10011  infsupneg  10012  zsupcllemstep  10679  nninfinf  10901  reuccatpfxs1  11541  fimaxre2  12016  nfsum1  12147  nfsum  12148  fsumsplitf  12200  fsum2dlemstep  12226  fsum00  12254  nfcprod1  12346  nfcprod  12347  prodeq2  12349  fprod2dlemstep  12414  fprodsplitf  12424  fprodsplit1f  12426  fprodap0f  12428  fprodle  12432  bezoutlemmain  12800  bezoutlemzz  12804  bezout  12813  exmidunben  13375  ctiunctlemfo  13388  ctiunct  13389  gsumsnfdcmn  14257  mulcncf  15834  ellimc3apf  15886  limccnp2cntop  15903  bdsepnft  17118  bdsepnfALT  17120  bj-findis  17210  strcollnft  17215  strcollnfALT  17217  pw1nct  17238  isomninnlem  17285  trirec0  17300  iswomninnlem  17306  ismkvnnlem  17309  nfals  17351  nfrals  17352  nfalseu  17382  nfralseu  17383