Theorem nfan 1588

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

Syntax hints:   /\ wa 104   F/wnf 1483

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 1470  ax-gen 1472  ax-4 1533

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

This theorem is referenced by:  nf3an  1589  cbvex2  1946  nfsbxyt  1971  nfsbv  1975  sbcomxyyz  2000  nfsb4t  2042  clelab  2331  nfel  2357  2ralbida  2527  r19.29an  2648  reean  2675  nfrabw  2687  cbvrexfw  2729  cbvrexf  2731  cbvreu  2736  cbvrab  2770  ceqsex2  2813  vtocl2gaf  2840  rspce  2872  eqvincf  2898  elrabf  2927  elrab3t  2928  rexab2  2939  morex  2957  reu2  2961  rmo3f  2970  sbc2iegf  3069  rmo2ilem  3088  rmo3  3090  csbiebt  3133  csbie2t  3142  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  nfopd  3836  eluniab  3862  dfnfc2  3868  nfdisjv  4033  disjiun  4039  nfopab  4112  cbvopab  4115  cbvopab1  4117  cbvopab2  4118  cbvopab1s  4119  mpteq12f  4124  nfmpt  4136  cbvmptf  4138  cbvmpt  4139  repizf2  4206  nfpo  4348  nfso  4349  nfwe  4402  onintonm  4565  peano2  4643  nfxp  4702  opeliunxp  4730  nfco  4843  elrnmpt1  4929  nfimad  5031  iota2  5261  dffun4f  5287  nffun  5294  imadif  5354  funimaexglem  5357  nffn  5370  nff  5422  nff1  5479  nffo  5497  nff1o  5520  fun11iun  5543  nffvd  5588  fv3  5599  fmptco  5746  nfiso  5875  cbvriota  5910  riota2df  5920  riota5f  5924  nfoprab  5997  mpoeq123  6004  nfmpo  6014  cbvoprab1  6017  cbvoprab2  6018  cbvoprab12  6019  cbvoprab3  6021  cbvmpox  6023  ovmpodxf  6071  elovmporab  6146  elovmporab1w  6147  opabex3d  6206  opabex3  6207  uchoice  6223  dfoprab4f  6279  fmpox  6286  spc2ed  6319  cnvoprab  6320  f1od2  6321  opeliunxp2f  6324  nfrecs  6393  tfri3  6453  nffrec  6482  erovlem  6714  nfixpxy  6804  nfixp1  6805  xpf1o  6941  nneneq  6954  ac6sfi  6995  opabfi  7035  nfsup  7094  exmidomni  7244  fodjuomnilemdc  7246  ismkvnex  7257  mkvprop  7260  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  cc3  7380  caucvgsrlemgt1  7908  suplocsrlem  7921  axpre-suploclemres  8014  supinfneg  9716  infsupneg  9717  zsupcllemstep  10372  nninfinf  10588  fimaxre2  11538  nfsum1  11667  nfsum  11668  fsumsplitf  11719  fsum2dlemstep  11745  fsum00  11773  nfcprod1  11865  nfcprod  11866  prodeq2  11868  fprod2dlemstep  11933  fprodsplitf  11943  fprodsplit1f  11945  fprodap0f  11947  fprodle  11951  bezoutlemmain  12319  bezoutlemzz  12323  bezout  12332  exmidunben  12797  ctiunctlemfo  12810  ctiunct  12811  mulcncf  15080  ellimc3apf  15132  limccnp2cntop  15149  bdsepnft  15823  bdsepnfALT  15825  bj-findis  15915  strcollnft  15920  strcollnfALT  15922  pw1nct  15940  isomninnlem  15969  trirec0  15983  iswomninnlem  15988  ismkvnnlem  15991