Theorem nfan 1576

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 1575	1 |- F/ x ( ph /\ ps )

Syntax hints:   /\ wa 104   F/wnf 1471

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 1458  ax-gen 1460  ax-4 1521

This theorem depends on definitions:  df-bi 117  df-nf 1472

This theorem is referenced by:  nf3an  1577  cbvex2  1934  nfsbxyt  1959  nfsbv  1963  sbcomxyyz  1988  nfsb4t  2030  clelab  2319  nfel  2345  2ralbida  2515  r19.29an  2636  reean  2663  nfrabw  2675  cbvrexfw  2717  cbvrexf  2719  cbvreu  2724  cbvrab  2758  ceqsex2  2800  vtocl2gaf  2827  rspce  2859  eqvincf  2885  elrabf  2914  elrab3t  2915  rexab2  2926  morex  2944  reu2  2948  rmo3f  2957  sbc2iegf  3056  rmo2ilem  3075  rmo3  3077  csbiebt  3120  csbie2t  3129  cbvrexcsf  3144  cbvreucsf  3145  cbvrabcsf  3146  nfopd  3821  eluniab  3847  dfnfc2  3853  nfdisjv  4018  disjiun  4024  nfopab  4097  cbvopab  4100  cbvopab1  4102  cbvopab2  4103  cbvopab1s  4104  mpteq12f  4109  nfmpt  4121  cbvmptf  4123  cbvmpt  4124  repizf2  4191  nfpo  4332  nfso  4333  nfwe  4386  onintonm  4549  peano2  4627  nfxp  4686  opeliunxp  4714  nfco  4827  elrnmpt1  4913  nfimad  5014  iota2  5244  dffun4f  5270  nffun  5277  imadif  5334  funimaexglem  5337  nffn  5350  nff  5400  nff1  5457  nffo  5475  nff1o  5498  fun11iun  5521  nffvd  5566  fv3  5577  fmptco  5724  nfiso  5849  cbvriota  5884  riota2df  5894  riota5f  5898  nfoprab  5970  mpoeq123  5977  nfmpo  5987  cbvoprab1  5990  cbvoprab2  5991  cbvoprab12  5992  cbvoprab3  5994  cbvmpox  5996  ovmpodxf  6044  elovmporab  6118  elovmporab1w  6119  opabex3d  6173  opabex3  6174  uchoice  6190  dfoprab4f  6246  fmpox  6253  spc2ed  6286  cnvoprab  6287  f1od2  6288  opeliunxp2f  6291  nfrecs  6360  tfri3  6420  nffrec  6449  erovlem  6681  nfixpxy  6771  nfixp1  6772  xpf1o  6900  nneneq  6913  ac6sfi  6954  opabfi  6992  nfsup  7051  exmidomni  7201  fodjuomnilemdc  7203  ismkvnex  7214  mkvprop  7217  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  cc3  7328  caucvgsrlemgt1  7855  suplocsrlem  7868  axpre-suploclemres  7961  supinfneg  9660  infsupneg  9661  nninfinf  10514  fimaxre2  11370  nfsum1  11499  nfsum  11500  fsumsplitf  11551  fsum2dlemstep  11577  fsum00  11605  nfcprod1  11697  nfcprod  11698  prodeq2  11700  fprod2dlemstep  11765  fprodsplitf  11775  fprodsplit1f  11777  fprodap0f  11779  fprodle  11783  zsupcllemstep  12082  bezoutlemmain  12135  bezoutlemzz  12139  bezout  12148  exmidunben  12583  ctiunctlemfo  12596  ctiunct  12597  mulcncf  14762  ellimc3apf  14814  limccnp2cntop  14831  bdsepnft  15379  bdsepnfALT  15381  bj-findis  15471  strcollnft  15476  strcollnfALT  15478  pw1nct  15493  isomninnlem  15520  trirec0  15534  iswomninnlem  15539  ismkvnnlem  15542