Theorem nfan 1498

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

Syntax hints:   /\ wa 102   F/wnf 1390

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 1377  ax-gen 1379  ax-4 1441

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

This theorem is referenced by:  nf3an  1499  cbvex2  1839  nfsbxyt  1861  sbcomxyyz  1888  nfsb4t  1932  clelab  2204  nfel  2228  2ralbida  2388  reean  2523  nfrabxy  2535  cbvrexf  2573  cbvreu  2576  cbvrab  2600  ceqsex2  2640  vtocl2gaf  2666  rspce  2697  eqvincf  2721  elrabf  2748  elrab3t  2749  rexab2  2759  morex  2777  reu2  2781  sbc2iegf  2885  rmo2ilem  2904  rmo3  2906  csbiebt  2943  csbie2t  2951  cbvrexcsf  2966  cbvreucsf  2967  cbvrabcsf  2968  nfopd  3595  eluniab  3621  dfnfc2  3627  nfdisjv  3786  nfopab  3854  cbvopab  3857  cbvopab1  3859  cbvopab2  3860  cbvopab1s  3861  mpteq12f  3866  nfmpt  3878  cbvmpt  3880  repizf2  3944  nfpo  4064  nfso  4065  nfwe  4118  onintonm  4269  peano2  4344  nfxp  4397  opeliunxp  4421  nfco  4529  elrnmpt1  4613  nfimad  4707  iota2  4923  dffun4f  4948  nffun  4954  imadif  5010  funimaexglem  5013  nffn  5026  nff  5074  nff1  5121  nffo  5136  nff1o  5155  fun11iun  5178  nffvd  5218  fv3  5229  fmptco  5362  nfiso  5477  cbvriota  5509  riota2df  5519  riota5f  5523  nfoprab  5588  mpt2eq123  5595  nfmpt2  5604  cbvoprab1  5607  cbvoprab2  5608  cbvoprab12  5609  cbvoprab3  5611  cbvmpt2x  5613  ovmpt2dxf  5657  opabex3d  5779  opabex3  5780  dfoprab4f  5850  fmpt2x  5857  spc2ed  5885  cnvoprab  5886  f1od2  5887  nfrecs  5956  tfr1onlemaccex  5997  tfrcllemaccex  6010  tfri3  6016  nffrec  6045  erovlem  6264  xpf1o  6385  nneneq  6392  ac6sfi  6431  nfsup  6464  caucvgsrlemgt1  7033  supinfneg  8764  infsupneg  8765  fimaxre2  10247  nfsum1  10331  nfsum  10332  zsupcllemstep  10485  bezoutlemmain  10531  bezoutlemzz  10535  bezout  10544  bdsepnft  10836  bdsepnfALT  10838  bj-findis  10932  strcollnft  10937