Theorem nfan 1614

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

Syntax hints:   /\ wa 104   F/wnf 1509

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 1496  ax-gen 1498  ax-4 1559

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

This theorem is referenced by:  nf3an  1615  cbvex2  1974  nfsbxyt  1999  nfsbv  2003  sbcomxyyz  2028  nfsb4t  2070  clelab  2362  nfel  2395  2ralbida  2565  r19.29an  2687  reean  2714  nfrabw  2727  cbvrmow  2729  cbvrexfw  2770  cbvrexf  2772  cbvreu  2778  cbvrab  2813  ceqsex2  2857  vtocl2gaf  2884  rspce  2918  eqvincf  2945  elrabf  2974  elrab3t  2975  rexab2  2986  morex  3004  reu2  3008  rmo3f  3017  sbc2iegf  3116  reu8nf  3127  rmo2ilem  3136  rmo3  3138  csbiebt  3181  csbie2t  3190  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  rabsnifsb  3762  nfopd  3905  eluniab  3931  dfnfc2  3937  nfdisjv  4102  disjiun  4109  nfopab  4183  cbvopab  4186  cbvopab1  4188  cbvopab2  4189  cbvopab1s  4190  mpteq12f  4195  nfmpt  4207  cbvmptf  4209  cbvmpt  4210  repizf2  4280  nfpo  4427  nfso  4428  nfwe  4481  onintonm  4644  peano2  4722  nfxp  4781  opeliunxp  4810  nfco  4925  elrnmpt1  5013  nfimad  5115  iota2  5347  dffun4f  5373  nffun  5380  imadif  5441  funimaexglem  5444  nffn  5457  nff  5510  nff1  5576  nffo  5594  nff1o  5617  fun11iun  5640  nffvd  5687  fv3  5698  fmptco  5848  nfiso  5985  cbvriota  6023  riota2df  6033  riota5f  6038  nfoprab  6113  mpoeq123  6120  nfmpo  6130  cbvoprab1  6133  cbvoprab2  6134  cbvoprab12  6135  cbvoprab3  6137  cbvmpox  6139  ovmpodxf  6187  elovmporab  6262  elovmporab1w  6263  opabex3d  6323  opabex3  6324  funimass4f  6332  uchoice  6344  dfoprab4f  6400  fmpox  6409  spc2ed  6442  cnvoprab  6443  f1od2  6444  opeliunxp2f  6482  nfrecs  6551  tfri3  6611  nffrec  6640  erovlem  6874  nfixpxy  6965  nfixp1  6966  modom  7074  xpf1o  7110  nneneq  7124  ac6sfi  7168  opabfi  7213  nfsup  7296  exmidomni  7446  fodjuomnilemdc  7448  ismkvnex  7459  mkvprop  7462  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  cc3  7598  caucvgsrlemgt1  8126  suplocsrlem  8139  axpre-suploclemres  8232  supinfneg  9945  infsupneg  9946  zsupcllemstep  10611  nninfinf  10829  reuccatpfxs1  11464  fimaxre2  11937  nfsum1  12066  nfsum  12067  fsumsplitf  12119  fsum2dlemstep  12145  fsum00  12173  nfcprod1  12265  nfcprod  12266  prodeq2  12268  fprod2dlemstep  12333  fprodsplitf  12343  fprodsplit1f  12345  fprodap0f  12347  fprodle  12351  bezoutlemmain  12719  bezoutlemzz  12723  bezout  12732  exmidunben  13261  ctiunctlemfo  13274  ctiunct  13275  mulcncf  15599  ellimc3apf  15651  limccnp2cntop  15668  bdsepnft  16783  bdsepnfALT  16785  bj-findis  16875  strcollnft  16880  strcollnfALT  16882  pw1nct  16903  isomninnlem  16940  trirec0  16954  iswomninnlem  16960  ismkvnnlem  16963