Theorem nfan 1579

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

Syntax hints:   /\ wa 104   F/wnf 1474

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 1461  ax-gen 1463  ax-4 1524

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

This theorem is referenced by:  nf3an  1580  cbvex2  1937  nfsbxyt  1962  nfsbv  1966  sbcomxyyz  1991  nfsb4t  2033  clelab  2322  nfel  2348  2ralbida  2518  r19.29an  2639  reean  2666  nfrabw  2678  cbvrexfw  2720  cbvrexf  2722  cbvreu  2727  cbvrab  2761  ceqsex2  2804  vtocl2gaf  2831  rspce  2863  eqvincf  2889  elrabf  2918  elrab3t  2919  rexab2  2930  morex  2948  reu2  2952  rmo3f  2961  sbc2iegf  3060  rmo2ilem  3079  rmo3  3081  csbiebt  3124  csbie2t  3133  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  nfopd  3825  eluniab  3851  dfnfc2  3857  nfdisjv  4022  disjiun  4028  nfopab  4101  cbvopab  4104  cbvopab1  4106  cbvopab2  4107  cbvopab1s  4108  mpteq12f  4113  nfmpt  4125  cbvmptf  4127  cbvmpt  4128  repizf2  4195  nfpo  4336  nfso  4337  nfwe  4390  onintonm  4553  peano2  4631  nfxp  4690  opeliunxp  4718  nfco  4831  elrnmpt1  4917  nfimad  5018  iota2  5248  dffun4f  5274  nffun  5281  imadif  5338  funimaexglem  5341  nffn  5354  nff  5404  nff1  5461  nffo  5479  nff1o  5502  fun11iun  5525  nffvd  5570  fv3  5581  fmptco  5728  nfiso  5853  cbvriota  5888  riota2df  5898  riota5f  5902  nfoprab  5974  mpoeq123  5981  nfmpo  5991  cbvoprab1  5994  cbvoprab2  5995  cbvoprab12  5996  cbvoprab3  5998  cbvmpox  6000  ovmpodxf  6048  elovmporab  6123  elovmporab1w  6124  opabex3d  6178  opabex3  6179  uchoice  6195  dfoprab4f  6251  fmpox  6258  spc2ed  6291  cnvoprab  6292  f1od2  6293  opeliunxp2f  6296  nfrecs  6365  tfri3  6425  nffrec  6454  erovlem  6686  nfixpxy  6776  nfixp1  6777  xpf1o  6905  nneneq  6918  ac6sfi  6959  opabfi  6999  nfsup  7058  exmidomni  7208  fodjuomnilemdc  7210  ismkvnex  7221  mkvprop  7224  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  cc3  7335  caucvgsrlemgt1  7862  suplocsrlem  7875  axpre-suploclemres  7968  supinfneg  9669  infsupneg  9670  zsupcllemstep  10319  nninfinf  10535  fimaxre2  11392  nfsum1  11521  nfsum  11522  fsumsplitf  11573  fsum2dlemstep  11599  fsum00  11627  nfcprod1  11719  nfcprod  11720  prodeq2  11722  fprod2dlemstep  11787  fprodsplitf  11797  fprodsplit1f  11799  fprodap0f  11801  fprodle  11805  bezoutlemmain  12165  bezoutlemzz  12169  bezout  12178  exmidunben  12643  ctiunctlemfo  12656  ctiunct  12657  mulcncf  14844  ellimc3apf  14896  limccnp2cntop  14913  bdsepnft  15533  bdsepnfALT  15535  bj-findis  15625  strcollnft  15630  strcollnfALT  15632  pw1nct  15647  isomninnlem  15674  trirec0  15688  iswomninnlem  15693  ismkvnnlem  15696