Theorem nfan 1587

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

Syntax hints:   /\ wa 104   F/wnf 1482

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 1469  ax-gen 1471  ax-4 1532

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

This theorem is referenced by:  nf3an  1588  cbvex2  1945  nfsbxyt  1970  nfsbv  1974  sbcomxyyz  1999  nfsb4t  2041  clelab  2330  nfel  2356  2ralbida  2526  r19.29an  2647  reean  2674  nfrabw  2686  cbvrexfw  2728  cbvrexf  2730  cbvreu  2735  cbvrab  2769  ceqsex2  2812  vtocl2gaf  2839  rspce  2871  eqvincf  2897  elrabf  2926  elrab3t  2927  rexab2  2938  morex  2956  reu2  2960  rmo3f  2969  sbc2iegf  3068  rmo2ilem  3087  rmo3  3089  csbiebt  3132  csbie2t  3141  cbvrexcsf  3156  cbvreucsf  3157  cbvrabcsf  3158  nfopd  3835  eluniab  3861  dfnfc2  3867  nfdisjv  4032  disjiun  4038  nfopab  4111  cbvopab  4114  cbvopab1  4116  cbvopab2  4117  cbvopab1s  4118  mpteq12f  4123  nfmpt  4135  cbvmptf  4137  cbvmpt  4138  repizf2  4205  nfpo  4347  nfso  4348  nfwe  4401  onintonm  4564  peano2  4642  nfxp  4701  opeliunxp  4729  nfco  4842  elrnmpt1  4928  nfimad  5030  iota2  5260  dffun4f  5286  nffun  5293  imadif  5353  funimaexglem  5356  nffn  5369  nff  5421  nff1  5478  nffo  5496  nff1o  5519  fun11iun  5542  nffvd  5587  fv3  5598  fmptco  5745  nfiso  5874  cbvriota  5909  riota2df  5919  riota5f  5923  nfoprab  5996  mpoeq123  6003  nfmpo  6013  cbvoprab1  6016  cbvoprab2  6017  cbvoprab12  6018  cbvoprab3  6020  cbvmpox  6022  ovmpodxf  6070  elovmporab  6145  elovmporab1w  6146  opabex3d  6205  opabex3  6206  uchoice  6222  dfoprab4f  6278  fmpox  6285  spc2ed  6318  cnvoprab  6319  f1od2  6320  opeliunxp2f  6323  nfrecs  6392  tfri3  6452  nffrec  6481  erovlem  6713  nfixpxy  6803  nfixp1  6804  xpf1o  6940  nneneq  6953  ac6sfi  6994  opabfi  7034  nfsup  7093  exmidomni  7243  fodjuomnilemdc  7245  ismkvnex  7256  mkvprop  7259  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  cc3  7379  caucvgsrlemgt1  7907  suplocsrlem  7920  axpre-suploclemres  8013  supinfneg  9715  infsupneg  9716  zsupcllemstep  10370  nninfinf  10586  fimaxre2  11509  nfsum1  11638  nfsum  11639  fsumsplitf  11690  fsum2dlemstep  11716  fsum00  11744  nfcprod1  11836  nfcprod  11837  prodeq2  11839  fprod2dlemstep  11904  fprodsplitf  11914  fprodsplit1f  11916  fprodap0f  11918  fprodle  11922  bezoutlemmain  12290  bezoutlemzz  12294  bezout  12303  exmidunben  12768  ctiunctlemfo  12781  ctiunct  12782  mulcncf  15051  ellimc3apf  15103  limccnp2cntop  15120  bdsepnft  15785  bdsepnfALT  15787  bj-findis  15877  strcollnft  15882  strcollnfALT  15884  pw1nct  15902  isomninnlem  15931  trirec0  15945  iswomninnlem  15950  ismkvnnlem  15953