Theorem nfan 1576

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

Syntax hints:   /\ wa 104   F/wnf 1471

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 1458  ax-gen 1460  ax-4 1521

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

This theorem is referenced by:  nf3an  1577  cbvex2  1934  nfsbxyt  1959  nfsbv  1963  sbcomxyyz  1988  nfsb4t  2030  clelab  2319  nfel  2345  2ralbida  2515  r19.29an  2636  reean  2663  nfrabw  2675  cbvrexfw  2717  cbvrexf  2719  cbvreu  2724  cbvrab  2758  ceqsex2  2801  vtocl2gaf  2828  rspce  2860  eqvincf  2886  elrabf  2915  elrab3t  2916  rexab2  2927  morex  2945  reu2  2949  rmo3f  2958  sbc2iegf  3057  rmo2ilem  3076  rmo3  3078  csbiebt  3121  csbie2t  3130  cbvrexcsf  3145  cbvreucsf  3146  cbvrabcsf  3147  nfopd  3822  eluniab  3848  dfnfc2  3854  nfdisjv  4019  disjiun  4025  nfopab  4098  cbvopab  4101  cbvopab1  4103  cbvopab2  4104  cbvopab1s  4105  mpteq12f  4110  nfmpt  4122  cbvmptf  4124  cbvmpt  4125  repizf2  4192  nfpo  4333  nfso  4334  nfwe  4387  onintonm  4550  peano2  4628  nfxp  4687  opeliunxp  4715  nfco  4828  elrnmpt1  4914  nfimad  5015  iota2  5245  dffun4f  5271  nffun  5278  imadif  5335  funimaexglem  5338  nffn  5351  nff  5401  nff1  5458  nffo  5476  nff1o  5499  fun11iun  5522  nffvd  5567  fv3  5578  fmptco  5725  nfiso  5850  cbvriota  5885  riota2df  5895  riota5f  5899  nfoprab  5971  mpoeq123  5978  nfmpo  5988  cbvoprab1  5991  cbvoprab2  5992  cbvoprab12  5993  cbvoprab3  5995  cbvmpox  5997  ovmpodxf  6045  elovmporab  6120  elovmporab1w  6121  opabex3d  6175  opabex3  6176  uchoice  6192  dfoprab4f  6248  fmpox  6255  spc2ed  6288  cnvoprab  6289  f1od2  6290  opeliunxp2f  6293  nfrecs  6362  tfri3  6422  nffrec  6451  erovlem  6683  nfixpxy  6773  nfixp1  6774  xpf1o  6902  nneneq  6915  ac6sfi  6956  opabfi  6994  nfsup  7053  exmidomni  7203  fodjuomnilemdc  7205  ismkvnex  7216  mkvprop  7219  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  cc3  7330  caucvgsrlemgt1  7857  suplocsrlem  7870  axpre-suploclemres  7963  supinfneg  9663  infsupneg  9664  nninfinf  10517  fimaxre2  11373  nfsum1  11502  nfsum  11503  fsumsplitf  11554  fsum2dlemstep  11580  fsum00  11608  nfcprod1  11700  nfcprod  11701  prodeq2  11703  fprod2dlemstep  11768  fprodsplitf  11778  fprodsplit1f  11780  fprodap0f  11782  fprodle  11786  zsupcllemstep  12085  bezoutlemmain  12138  bezoutlemzz  12142  bezout  12151  exmidunben  12586  ctiunctlemfo  12599  ctiunct  12600  mulcncf  14787  ellimc3apf  14839  limccnp2cntop  14856  bdsepnft  15449  bdsepnfALT  15451  bj-findis  15541  strcollnft  15546  strcollnfALT  15548  pw1nct  15563  isomninnlem  15590  trirec0  15604  iswomninnlem  15609  ismkvnnlem  15612