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  3556  eluniab  3582  dfnfc2  3588  nfdisjv  3747  nfopab  3815  cbvopab  3818  cbvopab1  3820  cbvopab2  3821  cbvopab1s  3822  mpteq12f  3827  nfmpt  3839  cbvmpt  3841  repizf2  3905  nfpo  4028  nfso  4029  peano2  4260  nfxp  4313  opeliunxp  4337  nfco  4443  elrnmpt1  4527  nfimad  4619  iota2  4835  dffun4f  4859  nffun  4865  imadif  4920  funimaexglem  4923  nffn  4936  nff  4984  nff1  5031  nffo  5046  nff1o  5065  fun11iun  5088  nffvd  5128  fv3  5138  fmptco  5271  nfiso  5387  cbvriota  5418  riota2df  5428  riota5f  5432  nfoprab  5496  mpt2eq123  5503  nfmpt2  5512  cbvoprab1  5515  cbvoprab2  5516  cbvoprab12  5517  cbvoprab3  5519  cbvmpt2x  5521  ovmpt2dxf  5565  opabex3d  5687  opabex3  5688  dfoprab4f  5758  fmpt2x  5765  nfrecs  5860  tfri3  5891  erovlem  6127  bdsepnft  8940  bdsepnfALT  8942  bj-findis  9028  strcollnft  9033