Theorem nfan 1553

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

Syntax hints:   /\ wa 103   F/wnf 1448

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 1435  ax-gen 1437  ax-4 1498

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

This theorem is referenced by:  nf3an  1554  cbvex2  1910  nfsbxyt  1931  nfsbv  1935  sbcomxyyz  1960  nfsb4t  2002  clelab  2292  nfel  2317  2ralbida  2487  r19.29an  2608  reean  2634  nfrabxy  2646  cbvrexfw  2684  cbvrexf  2686  cbvreu  2690  cbvrab  2724  ceqsex2  2766  vtocl2gaf  2793  rspce  2825  eqvincf  2851  elrabf  2880  elrab3t  2881  rexab2  2892  morex  2910  reu2  2914  rmo3f  2923  sbc2iegf  3021  rmo2ilem  3040  rmo3  3042  csbiebt  3084  csbie2t  3093  cbvrexcsf  3108  cbvreucsf  3109  cbvrabcsf  3110  nfopd  3775  eluniab  3801  dfnfc2  3807  nfdisjv  3971  disjiun  3977  nfopab  4050  cbvopab  4053  cbvopab1  4055  cbvopab2  4056  cbvopab1s  4057  mpteq12f  4062  nfmpt  4074  cbvmptf  4076  cbvmpt  4077  repizf2  4141  nfpo  4279  nfso  4280  nfwe  4333  onintonm  4494  peano2  4572  nfxp  4631  opeliunxp  4659  nfco  4769  elrnmpt1  4855  nfimad  4955  iota2  5179  dffun4f  5204  nffun  5211  imadif  5268  funimaexglem  5271  nffn  5284  nff  5334  nff1  5391  nffo  5409  nff1o  5430  fun11iun  5453  nffvd  5498  fv3  5509  fmptco  5651  nfiso  5774  cbvriota  5808  riota2df  5818  riota5f  5822  nfoprab  5894  mpoeq123  5901  nfmpo  5911  cbvoprab1  5914  cbvoprab2  5915  cbvoprab12  5916  cbvoprab3  5918  cbvmpox  5920  ovmpodxf  5967  opabex3d  6089  opabex3  6090  dfoprab4f  6161  fmpox  6168  spc2ed  6201  cnvoprab  6202  f1od2  6203  opeliunxp2f  6206  nfrecs  6275  tfri3  6335  nffrec  6364  erovlem  6593  nfixpxy  6683  nfixp1  6684  xpf1o  6810  nneneq  6823  ac6sfi  6864  nfsup  6957  exmidomni  7106  fodjuomnilemdc  7108  ismkvnex  7119  mkvprop  7122  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  cc3  7209  caucvgsrlemgt1  7736  suplocsrlem  7749  axpre-suploclemres  7842  supinfneg  9533  infsupneg  9534  fimaxre2  11168  nfsum1  11297  nfsum  11298  fsumsplitf  11349  fsum2dlemstep  11375  fsum00  11403  nfcprod1  11495  nfcprod  11496  prodeq2  11498  fprod2dlemstep  11563  fprodsplitf  11573  fprodsplit1f  11575  fprodap0f  11577  fprodle  11581  zsupcllemstep  11878  bezoutlemmain  11931  bezoutlemzz  11935  bezout  11944  exmidunben  12359  ctiunctlemfo  12372  ctiunct  12373  mulcncf  13231  ellimc3apf  13269  limccnp2cntop  13286  bdsepnft  13769  bdsepnfALT  13771  bj-findis  13861  strcollnft  13866  strcollnfALT  13868  pw1nct  13883  isomninnlem  13909  trirec0  13923  iswomninnlem  13928  ismkvnnlem  13931