Theorem nfan 1497

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

Syntax hints:   /\ wa 102   F/wnf 1389

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440

This theorem depends on definitions:  df-bi 115  df-nf 1390

This theorem is referenced by:  nf3an  1498  cbvex2  1838  nfsbxyt  1860  sbcomxyyz  1887  nfsb4t  1931  clelab  2203  nfel  2227  2ralbida  2387  reean  2522  nfrabxy  2534  cbvrexf  2572  cbvreu  2575  cbvrab  2599  ceqsex2  2639  vtocl2gaf  2665  rspce  2696  eqvincf  2720  elrabf  2747  elrab3t  2748  rexab2  2758  morex  2776  reu2  2780  sbc2iegf  2884  rmo2ilem  2903  rmo3  2905  csbiebt  2942  csbie2t  2950  cbvrexcsf  2965  cbvreucsf  2966  cbvrabcsf  2967  nfopd  3587  eluniab  3613  dfnfc2  3619  nfdisjv  3778  nfopab  3846  cbvopab  3849  cbvopab1  3851  cbvopab2  3852  cbvopab1s  3853  mpteq12f  3858  nfmpt  3870  cbvmpt  3872  repizf2  3936  nfpo  4056  nfso  4057  nfwe  4110  onintonm  4261  peano2  4336  nfxp  4389  opeliunxp  4413  nfco  4519  elrnmpt1  4603  nfimad  4697  iota2  4913  dffun4f  4938  nffun  4944  imadif  4999  funimaexglem  5002  nffn  5015  nff  5063  nff1  5110  nffo  5125  nff1o  5144  fun11iun  5167  nffvd  5207  fv3  5218  fmptco  5351  nfiso  5466  cbvriota  5498  riota2df  5508  riota5f  5512  nfoprab  5577  mpt2eq123  5584  nfmpt2  5593  cbvoprab1  5596  cbvoprab2  5597  cbvoprab12  5598  cbvoprab3  5600  cbvmpt2x  5602  ovmpt2dxf  5646  opabex3d  5768  opabex3  5769  dfoprab4f  5839  fmpt2x  5846  spc2ed  5874  cnvoprab  5875  f1od2  5876  nfrecs  5945  tfri3  5976  nffrec  6005  erovlem  6221  nneneq  6343  ac6sfi  6379  nfsup  6405  caucvgsrlemgt1  6971  supinfneg  8683  infsupneg  8684  fimaxre2  10109  nfsum1  10193  nfsum  10194  zsupcllemstep  10341  bezoutlemmain  10387  bezoutlemzz  10391  bezout  10400  bdsepnft  10678  bdsepnfALT  10680  bj-findis  10774  strcollnft  10779