Theorem nfan 1558

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

Syntax hints:   /\ wa 103   F/wnf 1453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503

This theorem depends on definitions:  df-bi 116  df-nf 1454

This theorem is referenced by:  nf3an  1559  cbvex2  1915  nfsbxyt  1936  nfsbv  1940  sbcomxyyz  1965  nfsb4t  2007  clelab  2296  nfel  2321  2ralbida  2491  r19.29an  2612  reean  2638  nfrabxy  2650  cbvrexfw  2688  cbvrexf  2690  cbvreu  2694  cbvrab  2728  ceqsex2  2770  vtocl2gaf  2797  rspce  2829  eqvincf  2855  elrabf  2884  elrab3t  2885  rexab2  2896  morex  2914  reu2  2918  rmo3f  2927  sbc2iegf  3025  rmo2ilem  3044  rmo3  3046  csbiebt  3088  csbie2t  3097  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  nfopd  3782  eluniab  3808  dfnfc2  3814  nfdisjv  3978  disjiun  3984  nfopab  4057  cbvopab  4060  cbvopab1  4062  cbvopab2  4063  cbvopab1s  4064  mpteq12f  4069  nfmpt  4081  cbvmptf  4083  cbvmpt  4084  repizf2  4148  nfpo  4286  nfso  4287  nfwe  4340  onintonm  4501  peano2  4579  nfxp  4638  opeliunxp  4666  nfco  4776  elrnmpt1  4862  nfimad  4962  iota2  5188  dffun4f  5214  nffun  5221  imadif  5278  funimaexglem  5281  nffn  5294  nff  5344  nff1  5401  nffo  5419  nff1o  5440  fun11iun  5463  nffvd  5508  fv3  5519  fmptco  5662  nfiso  5785  cbvriota  5819  riota2df  5829  riota5f  5833  nfoprab  5905  mpoeq123  5912  nfmpo  5922  cbvoprab1  5925  cbvoprab2  5926  cbvoprab12  5927  cbvoprab3  5929  cbvmpox  5931  ovmpodxf  5978  opabex3d  6100  opabex3  6101  dfoprab4f  6172  fmpox  6179  spc2ed  6212  cnvoprab  6213  f1od2  6214  opeliunxp2f  6217  nfrecs  6286  tfri3  6346  nffrec  6375  erovlem  6605  nfixpxy  6695  nfixp1  6696  xpf1o  6822  nneneq  6835  ac6sfi  6876  nfsup  6969  exmidomni  7118  fodjuomnilemdc  7120  ismkvnex  7131  mkvprop  7134  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  cc3  7230  caucvgsrlemgt1  7757  suplocsrlem  7770  axpre-suploclemres  7863  supinfneg  9554  infsupneg  9555  fimaxre2  11190  nfsum1  11319  nfsum  11320  fsumsplitf  11371  fsum2dlemstep  11397  fsum00  11425  nfcprod1  11517  nfcprod  11518  prodeq2  11520  fprod2dlemstep  11585  fprodsplitf  11595  fprodsplit1f  11597  fprodap0f  11599  fprodle  11603  zsupcllemstep  11900  bezoutlemmain  11953  bezoutlemzz  11957  bezout  11966  exmidunben  12381  ctiunctlemfo  12394  ctiunct  12395  mulcncf  13385  ellimc3apf  13423  limccnp2cntop  13440  bdsepnft  13922  bdsepnfALT  13924  bj-findis  14014  strcollnft  14019  strcollnfALT  14021  pw1nct  14036  isomninnlem  14062  trirec0  14076  iswomninnlem  14081  ismkvnnlem  14084