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  1972  nfsbxyt  1997  nfsbv  2001  sbcomxyyz  2026  nfsb4t  2068  clelab  2360  nfel  2393  2ralbida  2563  r19.29an  2685  reean  2712  nfrabw  2725  cbvrmow  2727  cbvrexfw  2768  cbvrexf  2770  cbvreu  2776  cbvrab  2811  ceqsex2  2855  vtocl2gaf  2882  rspce  2916  eqvincf  2942  elrabf  2971  elrab3t  2972  rexab2  2983  morex  3001  reu2  3005  rmo3f  3014  sbc2iegf  3113  reu8nf  3124  rmo2ilem  3133  rmo3  3135  csbiebt  3178  csbie2t  3187  cbvrexcsf  3202  cbvreucsf  3203  cbvrabcsf  3204  rabsnifsb  3757  nfopd  3900  eluniab  3926  dfnfc2  3932  nfdisjv  4097  disjiun  4104  nfopab  4178  cbvopab  4181  cbvopab1  4183  cbvopab2  4184  cbvopab1s  4185  mpteq12f  4190  nfmpt  4202  cbvmptf  4204  cbvmpt  4205  repizf2  4275  nfpo  4422  nfso  4423  nfwe  4476  onintonm  4639  peano2  4717  nfxp  4776  opeliunxp  4805  nfco  4920  elrnmpt1  5008  nfimad  5110  iota2  5342  dffun4f  5368  nffun  5375  imadif  5436  funimaexglem  5439  nffn  5452  nff  5505  nff1  5571  nffo  5589  nff1o  5612  fun11iun  5635  nffvd  5682  fv3  5693  fmptco  5843  nfiso  5979  cbvriota  6015  riota2df  6025  riota5f  6030  nfoprab  6105  mpoeq123  6112  nfmpo  6122  cbvoprab1  6125  cbvoprab2  6126  cbvoprab12  6127  cbvoprab3  6129  cbvmpox  6131  ovmpodxf  6179  elovmporab  6254  elovmporab1w  6255  opabex3d  6314  opabex3  6315  uchoice  6331  dfoprab4f  6387  fmpox  6396  spc2ed  6429  cnvoprab  6430  f1od2  6431  opeliunxp2f  6469  nfrecs  6538  tfri3  6598  nffrec  6627  erovlem  6861  nfixpxy  6952  nfixp1  6953  modom  7061  xpf1o  7097  nneneq  7111  ac6sfi  7155  opabfi  7200  nfsup  7283  exmidomni  7433  fodjuomnilemdc  7435  ismkvnex  7446  mkvprop  7449  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  cc3  7582  caucvgsrlemgt1  8110  suplocsrlem  8123  axpre-suploclemres  8216  supinfneg  9927  infsupneg  9928  zsupcllemstep  10589  nninfinf  10805  reuccatpfxs1  11439  fimaxre2  11912  nfsum1  12041  nfsum  12042  fsumsplitf  12094  fsum2dlemstep  12120  fsum00  12148  nfcprod1  12240  nfcprod  12241  prodeq2  12243  fprod2dlemstep  12308  fprodsplitf  12318  fprodsplit1f  12320  fprodap0f  12322  fprodle  12326  bezoutlemmain  12694  bezoutlemzz  12698  bezout  12707  exmidunben  13177  ctiunctlemfo  13190  ctiunct  13191  mulcncf  15473  ellimc3apf  15525  limccnp2cntop  15542  bdsepnft  16657  bdsepnfALT  16659  bj-findis  16749  strcollnft  16754  strcollnfALT  16756  pw1nct  16777  isomninnlem  16814  trirec0  16828  iswomninnlem  16834  ismkvnnlem  16837