Theorem nfan 1454

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/xph
nfan.2	|- F/xps

Assertion

Ref	Expression
nfan	|- F/x(ph /\ ps)

Proof of Theorem nfan

Step	Hyp	Ref	Expression
1		nfan.1	. 2 |- F/xph
2		nfan.2	. . 3 |- F/xps
3	2	a1i 9	. 2 |- (ph -> F/xps)
4	1, 3	nfan1 1453	1 |- F/x(ph /\ ps)

Syntax hints:   /\ wa 97   F/wnf 1346

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397

This theorem depends on definitions:  df-bi 110  df-nf 1347

This theorem is referenced by:  nf3an  1455  cbvex2  1794  nfsbxyt  1816  sbcomxyyz  1843  nfsb4t  1887  clelab  2159  nfel  2183  2ralbida  2339  reean  2472  nfrabxy  2484  cbvrexf  2522  cbvreu  2525  cbvrab  2549  ceqsex2  2588  vtocl2gaf  2614  rspce  2645  eqvincf  2663  elrabf  2690  elrab3t  2691  rexab2  2701  morex  2719  reu2  2723  sbc2iegf  2822  rmo2ilem  2841  rmo3  2843  csbiebt  2880  csbie2t  2888  cbvrexcsf  2903  cbvreucsf  2904  cbvrabcsf  2905  nfopd  3557  eluniab  3583  dfnfc2  3589  nfdisjv  3748  nfopab  3816  cbvopab  3819  cbvopab1  3821  cbvopab2  3822  cbvopab1s  3823  mpteq12f  3828  nfmpt  3840  cbvmpt  3842  repizf2  3906  nfpo  4029  nfso  4030  peano2  4261  nfxp  4314  opeliunxp  4338  nfco  4444  elrnmpt1  4528  nfimad  4620  iota2  4836  dffun4f  4861  nffun  4867  imadif  4922  funimaexglem  4925  nffn  4938  nff  4986  nff1  5033  nffo  5048  nff1o  5067  fun11iun  5090  nffvd  5130  fv3  5140  fmptco  5273  nfiso  5389  cbvriota  5421  riota2df  5431  riota5f  5435  nfoprab  5499  mpt2eq123  5506  nfmpt2  5515  cbvoprab1  5518  cbvoprab2  5519  cbvoprab12  5520  cbvoprab3  5522  cbvmpt2x  5524  ovmpt2dxf  5568  opabex3d  5690  opabex3  5691  dfoprab4f  5761  fmpt2x  5768  nfrecs  5863  tfri3  5894  nffrec  5921  erovlem  6134  bdsepnft  9342  bdsepnfALT  9344  bj-findis  9439  strcollnft  9444