Theorem nfan 1579

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

Syntax hints:   /\ wa 104   F/wnf 1474

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 1461  ax-gen 1463  ax-4 1524

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

This theorem is referenced by:  nf3an  1580  cbvex2  1937  nfsbxyt  1962  nfsbv  1966  sbcomxyyz  1991  nfsb4t  2033  clelab  2322  nfel  2348  2ralbida  2518  r19.29an  2639  reean  2666  nfrabw  2678  cbvrexfw  2720  cbvrexf  2722  cbvreu  2727  cbvrab  2761  ceqsex2  2804  vtocl2gaf  2831  rspce  2863  eqvincf  2889  elrabf  2918  elrab3t  2919  rexab2  2930  morex  2948  reu2  2952  rmo3f  2961  sbc2iegf  3060  rmo2ilem  3079  rmo3  3081  csbiebt  3124  csbie2t  3133  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  nfopd  3826  eluniab  3852  dfnfc2  3858  nfdisjv  4023  disjiun  4029  nfopab  4102  cbvopab  4105  cbvopab1  4107  cbvopab2  4108  cbvopab1s  4109  mpteq12f  4114  nfmpt  4126  cbvmptf  4128  cbvmpt  4129  repizf2  4196  nfpo  4337  nfso  4338  nfwe  4391  onintonm  4554  peano2  4632  nfxp  4691  opeliunxp  4719  nfco  4832  elrnmpt1  4918  nfimad  5019  iota2  5249  dffun4f  5275  nffun  5282  imadif  5339  funimaexglem  5342  nffn  5355  nff  5407  nff1  5464  nffo  5482  nff1o  5505  fun11iun  5528  nffvd  5573  fv3  5584  fmptco  5731  nfiso  5856  cbvriota  5891  riota2df  5901  riota5f  5905  nfoprab  5978  mpoeq123  5985  nfmpo  5995  cbvoprab1  5998  cbvoprab2  5999  cbvoprab12  6000  cbvoprab3  6002  cbvmpox  6004  ovmpodxf  6052  elovmporab  6127  elovmporab1w  6128  opabex3d  6187  opabex3  6188  uchoice  6204  dfoprab4f  6260  fmpox  6267  spc2ed  6300  cnvoprab  6301  f1od2  6302  opeliunxp2f  6305  nfrecs  6374  tfri3  6434  nffrec  6463  erovlem  6695  nfixpxy  6785  nfixp1  6786  xpf1o  6914  nneneq  6927  ac6sfi  6968  opabfi  7008  nfsup  7067  exmidomni  7217  fodjuomnilemdc  7219  ismkvnex  7230  mkvprop  7233  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  cc3  7351  caucvgsrlemgt1  7879  suplocsrlem  7892  axpre-suploclemres  7985  supinfneg  9686  infsupneg  9687  zsupcllemstep  10336  nninfinf  10552  fimaxre2  11409  nfsum1  11538  nfsum  11539  fsumsplitf  11590  fsum2dlemstep  11616  fsum00  11644  nfcprod1  11736  nfcprod  11737  prodeq2  11739  fprod2dlemstep  11804  fprodsplitf  11814  fprodsplit1f  11816  fprodap0f  11818  fprodle  11822  bezoutlemmain  12190  bezoutlemzz  12194  bezout  12203  exmidunben  12668  ctiunctlemfo  12681  ctiunct  12682  mulcncf  14928  ellimc3apf  14980  limccnp2cntop  14997  bdsepnft  15617  bdsepnfALT  15619  bj-findis  15709  strcollnft  15714  strcollnfALT  15716  pw1nct  15734  isomninnlem  15761  trirec0  15775  iswomninnlem  15780  ismkvnnlem  15783