Theorem nfan 1589

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

Syntax hints:   /\ wa 104   F/wnf 1484

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 1471  ax-gen 1473  ax-4 1534

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

This theorem is referenced by:  nf3an  1590  cbvex2  1947  nfsbxyt  1972  nfsbv  1976  sbcomxyyz  2001  nfsb4t  2043  clelab  2332  nfel  2358  2ralbida  2528  r19.29an  2649  reean  2676  nfrabw  2688  cbvrexfw  2730  cbvrexf  2732  cbvreu  2737  cbvrab  2771  ceqsex2  2815  vtocl2gaf  2842  rspce  2876  eqvincf  2902  elrabf  2931  elrab3t  2932  rexab2  2943  morex  2961  reu2  2965  rmo3f  2974  sbc2iegf  3073  rmo2ilem  3092  rmo3  3094  csbiebt  3137  csbie2t  3146  cbvrexcsf  3161  cbvreucsf  3162  cbvrabcsf  3163  nfopd  3845  eluniab  3871  dfnfc2  3877  nfdisjv  4042  disjiun  4049  nfopab  4123  cbvopab  4126  cbvopab1  4128  cbvopab2  4129  cbvopab1s  4130  mpteq12f  4135  nfmpt  4147  cbvmptf  4149  cbvmpt  4150  repizf2  4217  nfpo  4361  nfso  4362  nfwe  4415  onintonm  4578  peano2  4656  nfxp  4715  opeliunxp  4743  nfco  4856  elrnmpt1  4943  nfimad  5045  iota2  5275  dffun4f  5301  nffun  5308  imadif  5368  funimaexglem  5371  nffn  5384  nff  5437  nff1  5496  nffo  5514  nff1o  5537  fun11iun  5560  nffvd  5606  fv3  5617  fmptco  5764  nfiso  5893  cbvriota  5928  riota2df  5938  riota5f  5942  nfoprab  6015  mpoeq123  6022  nfmpo  6032  cbvoprab1  6035  cbvoprab2  6036  cbvoprab12  6037  cbvoprab3  6039  cbvmpox  6041  ovmpodxf  6089  elovmporab  6164  elovmporab1w  6165  opabex3d  6224  opabex3  6225  uchoice  6241  dfoprab4f  6297  fmpox  6304  spc2ed  6337  cnvoprab  6338  f1od2  6339  opeliunxp2f  6342  nfrecs  6411  tfri3  6471  nffrec  6500  erovlem  6732  nfixpxy  6822  nfixp1  6823  xpf1o  6961  nneneq  6974  ac6sfi  7016  opabfi  7056  nfsup  7115  exmidomni  7265  fodjuomnilemdc  7267  ismkvnex  7278  mkvprop  7281  exmidfodomrlemr  7336  exmidfodomrlemrALT  7337  cc3  7410  caucvgsrlemgt1  7938  suplocsrlem  7951  axpre-suploclemres  8044  supinfneg  9746  infsupneg  9747  zsupcllemstep  10404  nninfinf  10620  fimaxre2  11623  nfsum1  11752  nfsum  11753  fsumsplitf  11804  fsum2dlemstep  11830  fsum00  11858  nfcprod1  11950  nfcprod  11951  prodeq2  11953  fprod2dlemstep  12018  fprodsplitf  12028  fprodsplit1f  12030  fprodap0f  12032  fprodle  12036  bezoutlemmain  12404  bezoutlemzz  12408  bezout  12417  exmidunben  12882  ctiunctlemfo  12895  ctiunct  12896  mulcncf  15165  ellimc3apf  15217  limccnp2cntop  15234  bdsepnft  15992  bdsepnfALT  15994  bj-findis  16084  strcollnft  16089  strcollnfALT  16091  pw1nct  16112  isomninnlem  16141  trirec0  16155  iswomninnlem  16160  ismkvnnlem  16163