Theorem nfan 1545

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

Syntax hints:   /\ wa 103   F/wnf 1440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-4 1490

This theorem depends on definitions:  df-bi 116  df-nf 1441

This theorem is referenced by:  nf3an  1546  cbvex2  1902  nfsbxyt  1923  nfsbv  1927  sbcomxyyz  1952  nfsb4t  1994  clelab  2283  nfel  2308  2ralbida  2478  r19.29an  2599  reean  2625  nfrabxy  2637  cbvrexf  2675  cbvreu  2678  cbvrab  2710  ceqsex2  2752  vtocl2gaf  2779  rspce  2811  eqvincf  2837  elrabf  2866  elrab3t  2867  rexab2  2878  morex  2896  reu2  2900  rmo3f  2909  sbc2iegf  3007  rmo2ilem  3026  rmo3  3028  csbiebt  3070  csbie2t  3079  cbvrexcsf  3094  cbvreucsf  3095  cbvrabcsf  3096  nfopd  3758  eluniab  3784  dfnfc2  3790  nfdisjv  3954  disjiun  3960  nfopab  4032  cbvopab  4035  cbvopab1  4037  cbvopab2  4038  cbvopab1s  4039  mpteq12f  4044  nfmpt  4056  cbvmptf  4058  cbvmpt  4059  repizf2  4122  nfpo  4260  nfso  4261  nfwe  4314  onintonm  4474  peano2  4552  nfxp  4610  opeliunxp  4638  nfco  4748  elrnmpt1  4834  nfimad  4934  iota2  5158  dffun4f  5183  nffun  5190  imadif  5247  funimaexglem  5250  nffn  5263  nff  5313  nff1  5370  nffo  5388  nff1o  5409  fun11iun  5432  nffvd  5477  fv3  5488  fmptco  5630  nfiso  5751  cbvriota  5784  riota2df  5794  riota5f  5798  nfoprab  5867  mpoeq123  5874  nfmpo  5884  cbvoprab1  5887  cbvoprab2  5888  cbvoprab12  5889  cbvoprab3  5891  cbvmpox  5893  ovmpodxf  5940  opabex3d  6063  opabex3  6064  dfoprab4f  6135  fmpox  6142  spc2ed  6174  cnvoprab  6175  f1od2  6176  opeliunxp2f  6179  nfrecs  6248  tfri3  6308  nffrec  6337  erovlem  6565  nfixpxy  6655  nfixp1  6656  xpf1o  6782  nneneq  6795  ac6sfi  6836  nfsup  6928  exmidomni  7068  fodjuomnilemdc  7070  ismkvnex  7081  mkvprop  7084  exmidfodomrlemr  7120  exmidfodomrlemrALT  7121  cc3  7171  caucvgsrlemgt1  7698  suplocsrlem  7711  axpre-suploclemres  7804  supinfneg  9489  infsupneg  9490  fimaxre2  11108  nfsum1  11235  nfsum  11236  fsumsplitf  11287  fsum2dlemstep  11313  fsum00  11341  nfcprod1  11433  nfcprod  11434  prodeq2  11436  fprod2dlemstep  11501  fprodsplitf  11511  fprodsplit1f  11513  fprodap0f  11515  fprodle  11519  zsupcllemstep  11813  bezoutlemmain  11862  bezoutlemzz  11866  bezout  11875  exmidunben  12127  ctiunctlemfo  12140  ctiunct  12141  mulcncf  12951  ellimc3apf  12989  limccnp2cntop  13006  bdsepnft  13422  bdsepnfALT  13424  bj-findis  13514  strcollnft  13519  strcollnfALT  13521  pw1nct  13536  isomninnlem  13564  trirec0  13578  iswomninnlem  13583  ismkvnnlem  13586