Theorem nfan 1613

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

Syntax hints:   /\ wa 104   F/wnf 1508

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 1495  ax-gen 1497  ax-4 1558

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

This theorem is referenced by:  nf3an  1614  cbvex2  1971  nfsbxyt  1996  nfsbv  2000  sbcomxyyz  2025  nfsb4t  2067  clelab  2357  nfel  2383  2ralbida  2553  r19.29an  2675  reean  2702  nfrabw  2714  cbvrmow  2716  cbvrexfw  2757  cbvrexf  2759  cbvreu  2765  cbvrab  2800  ceqsex2  2844  vtocl2gaf  2871  rspce  2905  eqvincf  2931  elrabf  2960  elrab3t  2961  rexab2  2972  morex  2990  reu2  2994  rmo3f  3003  sbc2iegf  3102  reu8nf  3113  rmo2ilem  3122  rmo3  3124  csbiebt  3167  csbie2t  3176  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  rabsnifsb  3737  nfopd  3879  eluniab  3905  dfnfc2  3911  nfdisjv  4076  disjiun  4083  nfopab  4157  cbvopab  4160  cbvopab1  4162  cbvopab2  4163  cbvopab1s  4164  mpteq12f  4169  nfmpt  4181  cbvmptf  4183  cbvmpt  4184  repizf2  4252  nfpo  4398  nfso  4399  nfwe  4452  onintonm  4615  peano2  4693  nfxp  4752  opeliunxp  4781  nfco  4895  elrnmpt1  4983  nfimad  5085  iota2  5316  dffun4f  5342  nffun  5349  imadif  5410  funimaexglem  5413  nffn  5426  nff  5479  nff1  5540  nffo  5558  nff1o  5581  fun11iun  5604  nffvd  5651  fv3  5662  fmptco  5813  nfiso  5946  cbvriota  5982  riota2df  5992  riota5f  5997  nfoprab  6072  mpoeq123  6079  nfmpo  6089  cbvoprab1  6092  cbvoprab2  6093  cbvoprab12  6094  cbvoprab3  6096  cbvmpox  6098  ovmpodxf  6146  elovmporab  6221  elovmporab1w  6222  opabex3d  6282  opabex3  6283  uchoice  6299  dfoprab4f  6355  fmpox  6364  spc2ed  6397  cnvoprab  6398  f1od2  6399  opeliunxp2f  6403  nfrecs  6472  tfri3  6532  nffrec  6561  erovlem  6795  nfixpxy  6885  nfixp1  6886  modom  6993  xpf1o  7029  nneneq  7042  ac6sfi  7086  opabfi  7131  nfsup  7190  exmidomni  7340  fodjuomnilemdc  7342  ismkvnex  7353  mkvprop  7356  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  cc3  7486  caucvgsrlemgt1  8014  suplocsrlem  8027  axpre-suploclemres  8120  supinfneg  9828  infsupneg  9829  zsupcllemstep  10488  nninfinf  10704  reuccatpfxs1  11327  fimaxre2  11787  nfsum1  11916  nfsum  11917  fsumsplitf  11968  fsum2dlemstep  11994  fsum00  12022  nfcprod1  12114  nfcprod  12115  prodeq2  12117  fprod2dlemstep  12182  fprodsplitf  12192  fprodsplit1f  12194  fprodap0f  12196  fprodle  12200  bezoutlemmain  12568  bezoutlemzz  12572  bezout  12581  exmidunben  13046  ctiunctlemfo  13059  ctiunct  13060  mulcncf  15331  ellimc3apf  15383  limccnp2cntop  15400  bdsepnft  16482  bdsepnfALT  16484  bj-findis  16574  strcollnft  16579  strcollnfALT  16581  pw1nct  16604  isomninnlem  16634  trirec0  16648  iswomninnlem  16653  ismkvnnlem  16656