Theorem nfan 1611

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

Syntax hints:   /\ wa 104   F/wnf 1506

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 1493  ax-gen 1495  ax-4 1556

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

This theorem is referenced by:  nf3an  1612  cbvex2  1969  nfsbxyt  1994  nfsbv  1998  sbcomxyyz  2023  nfsb4t  2065  clelab  2355  nfel  2381  2ralbida  2551  r19.29an  2673  reean  2700  nfrabw  2712  cbvrmow  2714  cbvrexfw  2755  cbvrexf  2757  cbvreu  2763  cbvrab  2797  ceqsex2  2841  vtocl2gaf  2868  rspce  2902  eqvincf  2928  elrabf  2957  elrab3t  2958  rexab2  2969  morex  2987  reu2  2991  rmo3f  3000  sbc2iegf  3099  reu8nf  3110  rmo2ilem  3119  rmo3  3121  csbiebt  3164  csbie2t  3173  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  nfopd  3874  eluniab  3900  dfnfc2  3906  nfdisjv  4071  disjiun  4078  nfopab  4152  cbvopab  4155  cbvopab1  4157  cbvopab2  4158  cbvopab1s  4159  mpteq12f  4164  nfmpt  4176  cbvmptf  4178  cbvmpt  4179  repizf2  4246  nfpo  4392  nfso  4393  nfwe  4446  onintonm  4609  peano2  4687  nfxp  4746  opeliunxp  4774  nfco  4887  elrnmpt1  4975  nfimad  5077  iota2  5308  dffun4f  5334  nffun  5341  imadif  5401  funimaexglem  5404  nffn  5417  nff  5470  nff1  5531  nffo  5549  nff1o  5572  fun11iun  5595  nffvd  5641  fv3  5652  fmptco  5803  nfiso  5936  cbvriota  5972  riota2df  5982  riota5f  5987  nfoprab  6062  mpoeq123  6069  nfmpo  6079  cbvoprab1  6082  cbvoprab2  6083  cbvoprab12  6084  cbvoprab3  6086  cbvmpox  6088  ovmpodxf  6136  elovmporab  6211  elovmporab1w  6212  opabex3d  6272  opabex3  6273  uchoice  6289  dfoprab4f  6345  fmpox  6352  spc2ed  6385  cnvoprab  6386  f1od2  6387  opeliunxp2f  6390  nfrecs  6459  tfri3  6519  nffrec  6548  erovlem  6782  nfixpxy  6872  nfixp1  6873  xpf1o  7013  nneneq  7026  ac6sfi  7068  opabfi  7111  nfsup  7170  exmidomni  7320  fodjuomnilemdc  7322  ismkvnex  7333  mkvprop  7336  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  cc3  7465  caucvgsrlemgt1  7993  suplocsrlem  8006  axpre-suploclemres  8099  supinfneg  9802  infsupneg  9803  zsupcllemstep  10461  nninfinf  10677  reuccatpfxs1  11294  fimaxre2  11753  nfsum1  11882  nfsum  11883  fsumsplitf  11934  fsum2dlemstep  11960  fsum00  11988  nfcprod1  12080  nfcprod  12081  prodeq2  12083  fprod2dlemstep  12148  fprodsplitf  12158  fprodsplit1f  12160  fprodap0f  12162  fprodle  12166  bezoutlemmain  12534  bezoutlemzz  12538  bezout  12547  exmidunben  13012  ctiunctlemfo  13025  ctiunct  13026  mulcncf  15297  ellimc3apf  15349  limccnp2cntop  15366  bdsepnft  16305  bdsepnfALT  16307  bj-findis  16397  strcollnft  16402  strcollnfALT  16404  pw1nct  16428  isomninnlem  16458  trirec0  16472  iswomninnlem  16477  ismkvnnlem  16480