Theorem nfan 1457

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

Syntax hints:   /\ wa 97   F/wnf 1349

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 1336  ax-gen 1338  ax-4 1400

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

This theorem is referenced by:  nf3an  1458  cbvex2  1797  nfsbxyt  1819  sbcomxyyz  1846  nfsb4t  1890  clelab  2162  nfel  2186  2ralbida  2345  reean  2478  nfrabxy  2490  cbvrexf  2528  cbvreu  2531  cbvrab  2555  ceqsex2  2594  vtocl2gaf  2620  rspce  2651  eqvincf  2669  elrabf  2696  elrab3t  2697  rexab2  2707  morex  2725  reu2  2729  sbc2iegf  2828  rmo2ilem  2847  rmo3  2849  csbiebt  2886  csbie2t  2894  cbvrexcsf  2909  cbvreucsf  2910  cbvrabcsf  2911  nfopd  3566  eluniab  3592  dfnfc2  3598  nfdisjv  3757  nfopab  3825  cbvopab  3828  cbvopab1  3830  cbvopab2  3831  cbvopab1s  3832  mpteq12f  3837  nfmpt  3849  cbvmpt  3851  repizf2  3915  nfpo  4038  nfso  4039  nfwe  4092  onintonm  4243  peano2  4318  nfxp  4371  opeliunxp  4395  nfco  4501  elrnmpt1  4585  nfimad  4677  iota2  4893  dffun4f  4918  nffun  4924  imadif  4979  funimaexglem  4982  nffn  4995  nff  5043  nff1  5090  nffo  5105  nff1o  5124  fun11iun  5147  nffvd  5187  fv3  5197  fmptco  5330  nfiso  5446  cbvriota  5478  riota2df  5488  riota5f  5492  nfoprab  5557  mpt2eq123  5564  nfmpt2  5573  cbvoprab1  5576  cbvoprab2  5577  cbvoprab12  5578  cbvoprab3  5580  cbvmpt2x  5582  ovmpt2dxf  5626  opabex3d  5748  opabex3  5749  dfoprab4f  5819  fmpt2x  5826  nfrecs  5922  tfri3  5953  nffrec  5982  erovlem  6198  nneneq  6320  ac6sfi  6352  caucvgsrlemgt1  6879  nfsum1  9875  nfsum  9876  bdsepnft  10007  bdsepnfALT  10009  bj-findis  10104  strcollnft  10109