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  3873  eluniab  3899  dfnfc2  3905  nfdisjv  4070  disjiun  4077  nfopab  4151  cbvopab  4154  cbvopab1  4156  cbvopab2  4157  cbvopab1s  4158  mpteq12f  4163  nfmpt  4175  cbvmptf  4177  cbvmpt  4178  repizf2  4245  nfpo  4391  nfso  4392  nfwe  4445  onintonm  4608  peano2  4686  nfxp  4745  opeliunxp  4773  nfco  4886  elrnmpt1  4974  nfimad  5076  iota2  5307  dffun4f  5333  nffun  5340  imadif  5400  funimaexglem  5403  nffn  5416  nff  5469  nff1  5528  nffo  5546  nff1o  5569  fun11iun  5592  nffvd  5638  fv3  5649  fmptco  5800  nfiso  5929  cbvriota  5965  riota2df  5975  riota5f  5980  nfoprab  6055  mpoeq123  6062  nfmpo  6072  cbvoprab1  6075  cbvoprab2  6076  cbvoprab12  6077  cbvoprab3  6079  cbvmpox  6081  ovmpodxf  6129  elovmporab  6204  elovmporab1w  6205  opabex3d  6264  opabex3  6265  uchoice  6281  dfoprab4f  6337  fmpox  6344  spc2ed  6377  cnvoprab  6378  f1od2  6379  opeliunxp2f  6382  nfrecs  6451  tfri3  6511  nffrec  6540  erovlem  6772  nfixpxy  6862  nfixp1  6863  xpf1o  7001  nneneq  7014  ac6sfi  7056  opabfi  7096  nfsup  7155  exmidomni  7305  fodjuomnilemdc  7307  ismkvnex  7318  mkvprop  7321  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  cc3  7450  caucvgsrlemgt1  7978  suplocsrlem  7991  axpre-suploclemres  8084  supinfneg  9786  infsupneg  9787  zsupcllemstep  10444  nninfinf  10660  reuccatpfxs1  11274  fimaxre2  11733  nfsum1  11862  nfsum  11863  fsumsplitf  11914  fsum2dlemstep  11940  fsum00  11968  nfcprod1  12060  nfcprod  12061  prodeq2  12063  fprod2dlemstep  12128  fprodsplitf  12138  fprodsplit1f  12140  fprodap0f  12142  fprodle  12146  bezoutlemmain  12514  bezoutlemzz  12518  bezout  12527  exmidunben  12992  ctiunctlemfo  13005  ctiunct  13006  mulcncf  15276  ellimc3apf  15328  limccnp2cntop  15345  bdsepnft  16208  bdsepnfALT  16210  bj-findis  16300  strcollnft  16305  strcollnfALT  16307  pw1nct  16328  isomninnlem  16357  trirec0  16371  iswomninnlem  16376  ismkvnnlem  16379