Theorem nfan 1587

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

Syntax hints:   /\ wa 104   F/wnf 1482

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 1469  ax-gen 1471  ax-4 1532

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

This theorem is referenced by:  nf3an  1588  cbvex2  1945  nfsbxyt  1970  nfsbv  1974  sbcomxyyz  1999  nfsb4t  2041  clelab  2330  nfel  2356  2ralbida  2526  r19.29an  2647  reean  2674  nfrabw  2686  cbvrexfw  2728  cbvrexf  2730  cbvreu  2735  cbvrab  2769  ceqsex2  2812  vtocl2gaf  2839  rspce  2871  eqvincf  2897  elrabf  2926  elrab3t  2927  rexab2  2938  morex  2956  reu2  2960  rmo3f  2969  sbc2iegf  3068  rmo2ilem  3087  rmo3  3089  csbiebt  3132  csbie2t  3141  cbvrexcsf  3156  cbvreucsf  3157  cbvrabcsf  3158  nfopd  3835  eluniab  3861  dfnfc2  3867  nfdisjv  4032  disjiun  4038  nfopab  4111  cbvopab  4114  cbvopab1  4116  cbvopab2  4117  cbvopab1s  4118  mpteq12f  4123  nfmpt  4135  cbvmptf  4137  cbvmpt  4138  repizf2  4205  nfpo  4347  nfso  4348  nfwe  4401  onintonm  4564  peano2  4642  nfxp  4701  opeliunxp  4729  nfco  4842  elrnmpt1  4928  nfimad  5030  iota2  5260  dffun4f  5286  nffun  5293  imadif  5353  funimaexglem  5356  nffn  5369  nff  5421  nff1  5478  nffo  5496  nff1o  5519  fun11iun  5542  nffvd  5587  fv3  5598  fmptco  5745  nfiso  5874  cbvriota  5909  riota2df  5919  riota5f  5923  nfoprab  5996  mpoeq123  6003  nfmpo  6013  cbvoprab1  6016  cbvoprab2  6017  cbvoprab12  6018  cbvoprab3  6020  cbvmpox  6022  ovmpodxf  6070  elovmporab  6145  elovmporab1w  6146  opabex3d  6205  opabex3  6206  uchoice  6222  dfoprab4f  6278  fmpox  6285  spc2ed  6318  cnvoprab  6319  f1od2  6320  opeliunxp2f  6323  nfrecs  6392  tfri3  6452  nffrec  6481  erovlem  6713  nfixpxy  6803  nfixp1  6804  xpf1o  6940  nneneq  6953  ac6sfi  6994  opabfi  7034  nfsup  7093  exmidomni  7243  fodjuomnilemdc  7245  ismkvnex  7256  mkvprop  7259  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  cc3  7379  caucvgsrlemgt1  7907  suplocsrlem  7920  axpre-suploclemres  8013  supinfneg  9715  infsupneg  9716  zsupcllemstep  10370  nninfinf  10586  fimaxre2  11480  nfsum1  11609  nfsum  11610  fsumsplitf  11661  fsum2dlemstep  11687  fsum00  11715  nfcprod1  11807  nfcprod  11808  prodeq2  11810  fprod2dlemstep  11875  fprodsplitf  11885  fprodsplit1f  11887  fprodap0f  11889  fprodle  11893  bezoutlemmain  12261  bezoutlemzz  12265  bezout  12274  exmidunben  12739  ctiunctlemfo  12752  ctiunct  12753  mulcncf  15022  ellimc3apf  15074  limccnp2cntop  15091  bdsepnft  15756  bdsepnfALT  15758  bj-findis  15848  strcollnft  15853  strcollnfALT  15855  pw1nct  15873  isomninnlem  15902  trirec0  15916  iswomninnlem  15921  ismkvnnlem  15924