Theorem nfan 1565

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

Syntax hints:   /\ wa 104   F/wnf 1460

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 1447  ax-gen 1449  ax-4 1510

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

This theorem is referenced by:  nf3an  1566  cbvex2  1922  nfsbxyt  1943  nfsbv  1947  sbcomxyyz  1972  nfsb4t  2014  clelab  2303  nfel  2328  2ralbida  2498  r19.29an  2619  reean  2646  nfrabxy  2658  cbvrexfw  2696  cbvrexf  2698  cbvreu  2702  cbvrab  2736  ceqsex2  2778  vtocl2gaf  2805  rspce  2837  eqvincf  2863  elrabf  2892  elrab3t  2893  rexab2  2904  morex  2922  reu2  2926  rmo3f  2935  sbc2iegf  3034  rmo2ilem  3053  rmo3  3055  csbiebt  3097  csbie2t  3106  cbvrexcsf  3121  cbvreucsf  3122  cbvrabcsf  3123  nfopd  3796  eluniab  3822  dfnfc2  3828  nfdisjv  3993  disjiun  3999  nfopab  4072  cbvopab  4075  cbvopab1  4077  cbvopab2  4078  cbvopab1s  4079  mpteq12f  4084  nfmpt  4096  cbvmptf  4098  cbvmpt  4099  repizf2  4163  nfpo  4302  nfso  4303  nfwe  4356  onintonm  4517  peano2  4595  nfxp  4654  opeliunxp  4682  nfco  4793  elrnmpt1  4879  nfimad  4980  iota2  5207  dffun4f  5233  nffun  5240  imadif  5297  funimaexglem  5300  nffn  5313  nff  5363  nff1  5420  nffo  5438  nff1o  5460  fun11iun  5483  nffvd  5528  fv3  5539  fmptco  5683  nfiso  5807  cbvriota  5841  riota2df  5851  riota5f  5855  nfoprab  5927  mpoeq123  5934  nfmpo  5944  cbvoprab1  5947  cbvoprab2  5948  cbvoprab12  5949  cbvoprab3  5951  cbvmpox  5953  ovmpodxf  6000  opabex3d  6122  opabex3  6123  dfoprab4f  6194  fmpox  6201  spc2ed  6234  cnvoprab  6235  f1od2  6236  opeliunxp2f  6239  nfrecs  6308  tfri3  6368  nffrec  6397  erovlem  6627  nfixpxy  6717  nfixp1  6718  xpf1o  6844  nneneq  6857  ac6sfi  6898  nfsup  6991  exmidomni  7140  fodjuomnilemdc  7142  ismkvnex  7153  mkvprop  7156  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  cc3  7267  caucvgsrlemgt1  7794  suplocsrlem  7807  axpre-suploclemres  7900  supinfneg  9595  infsupneg  9596  fimaxre2  11235  nfsum1  11364  nfsum  11365  fsumsplitf  11416  fsum2dlemstep  11442  fsum00  11470  nfcprod1  11562  nfcprod  11563  prodeq2  11565  fprod2dlemstep  11630  fprodsplitf  11640  fprodsplit1f  11642  fprodap0f  11644  fprodle  11648  zsupcllemstep  11946  bezoutlemmain  11999  bezoutlemzz  12003  bezout  12012  exmidunben  12427  ctiunctlemfo  12440  ctiunct  12441  mulcncf  14094  ellimc3apf  14132  limccnp2cntop  14149  bdsepnft  14642  bdsepnfALT  14644  bj-findis  14734  strcollnft  14739  strcollnfALT  14741  pw1nct  14755  isomninnlem  14781  trirec0  14795  iswomninnlem  14800  ismkvnnlem  14803