Theorem nfan 1611

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

Syntax hints:   /\ wa 104   F/wnf 1506

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 1493  ax-gen 1495  ax-4 1556

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

This theorem is referenced by:  nf3an  1612  cbvex2  1969  nfsbxyt  1994  nfsbv  1998  sbcomxyyz  2023  nfsb4t  2065  clelab  2355  nfel  2381  2ralbida  2551  r19.29an  2673  reean  2700  nfrabw  2712  cbvrmow  2714  cbvrexfw  2755  cbvrexf  2757  cbvreu  2763  cbvrab  2798  ceqsex2  2842  vtocl2gaf  2869  rspce  2903  eqvincf  2929  elrabf  2958  elrab3t  2959  rexab2  2970  morex  2988  reu2  2992  rmo3f  3001  sbc2iegf  3100  reu8nf  3111  rmo2ilem  3120  rmo3  3122  csbiebt  3165  csbie2t  3174  cbvrexcsf  3189  cbvreucsf  3190  cbvrabcsf  3191  rabsnifsb  3735  nfopd  3877  eluniab  3903  dfnfc2  3909  nfdisjv  4074  disjiun  4081  nfopab  4155  cbvopab  4158  cbvopab1  4160  cbvopab2  4161  cbvopab1s  4162  mpteq12f  4167  nfmpt  4179  cbvmptf  4181  cbvmpt  4182  repizf2  4250  nfpo  4396  nfso  4397  nfwe  4450  onintonm  4613  peano2  4691  nfxp  4750  opeliunxp  4779  nfco  4893  elrnmpt1  4981  nfimad  5083  iota2  5314  dffun4f  5340  nffun  5347  imadif  5407  funimaexglem  5410  nffn  5423  nff  5476  nff1  5537  nffo  5555  nff1o  5578  fun11iun  5601  nffvd  5647  fv3  5658  fmptco  5809  nfiso  5942  cbvriota  5978  riota2df  5988  riota5f  5993  nfoprab  6068  mpoeq123  6075  nfmpo  6085  cbvoprab1  6088  cbvoprab2  6089  cbvoprab12  6090  cbvoprab3  6092  cbvmpox  6094  ovmpodxf  6142  elovmporab  6217  elovmporab1w  6218  opabex3d  6278  opabex3  6279  uchoice  6295  dfoprab4f  6351  fmpox  6360  spc2ed  6393  cnvoprab  6394  f1od2  6395  opeliunxp2f  6399  nfrecs  6468  tfri3  6528  nffrec  6557  erovlem  6791  nfixpxy  6881  nfixp1  6882  modom  6989  xpf1o  7025  nneneq  7038  ac6sfi  7080  opabfi  7123  nfsup  7182  exmidomni  7332  fodjuomnilemdc  7334  ismkvnex  7345  mkvprop  7348  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  cc3  7477  caucvgsrlemgt1  8005  suplocsrlem  8018  axpre-suploclemres  8111  supinfneg  9819  infsupneg  9820  zsupcllemstep  10479  nninfinf  10695  reuccatpfxs1  11318  fimaxre2  11778  nfsum1  11907  nfsum  11908  fsumsplitf  11959  fsum2dlemstep  11985  fsum00  12013  nfcprod1  12105  nfcprod  12106  prodeq2  12108  fprod2dlemstep  12173  fprodsplitf  12183  fprodsplit1f  12185  fprodap0f  12187  fprodle  12191  bezoutlemmain  12559  bezoutlemzz  12563  bezout  12572  exmidunben  13037  ctiunctlemfo  13050  ctiunct  13051  mulcncf  15322  ellimc3apf  15374  limccnp2cntop  15391  bdsepnft  16418  bdsepnfALT  16420  bj-findis  16510  strcollnft  16515  strcollnfALT  16517  pw1nct  16540  isomninnlem  16570  trirec0  16584  iswomninnlem  16589  ismkvnnlem  16592