Theorem nfan 1576

Description: If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 ∧ 𝜓). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.)

Hypotheses

Ref	Expression
nfan.1	⊢ Ⅎ𝑥𝜑
nfan.2	⊢ Ⅎ𝑥𝜓

Assertion

Ref	Expression
nfan	⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Proof of Theorem nfan

Step	Hyp	Ref	Expression
1		nfan.1	. 2 ⊢ Ⅎ𝑥𝜑
2		nfan.2	. . 3 ⊢ Ⅎ𝑥𝜓
3	2	a1i 9	. 2 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	1, 3	nfan1 1575	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Syntax hints:   ∧ wa 104  Ⅎwnf 1471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-4 1521

This theorem depends on definitions:  df-bi 117  df-nf 1472

This theorem is referenced by:  nf3an  1577  cbvex2  1934  nfsbxyt  1955  nfsbv  1959  sbcomxyyz  1984  nfsb4t  2026  clelab  2315  nfel  2341  2ralbida  2511  r19.29an  2632  reean  2659  nfrabxy  2671  cbvrexfw  2709  cbvrexf  2711  cbvreu  2716  cbvrab  2750  ceqsex2  2792  vtocl2gaf  2819  rspce  2851  eqvincf  2877  elrabf  2906  elrab3t  2907  rexab2  2918  morex  2936  reu2  2940  rmo3f  2949  sbc2iegf  3048  rmo2ilem  3067  rmo3  3069  csbiebt  3111  csbie2t  3120  cbvrexcsf  3135  cbvreucsf  3136  cbvrabcsf  3137  nfopd  3810  eluniab  3836  dfnfc2  3842  nfdisjv  4007  disjiun  4013  nfopab  4086  cbvopab  4089  cbvopab1  4091  cbvopab2  4092  cbvopab1s  4093  mpteq12f  4098  nfmpt  4110  cbvmptf  4112  cbvmpt  4113  repizf2  4180  nfpo  4319  nfso  4320  nfwe  4373  onintonm  4534  peano2  4612  nfxp  4671  opeliunxp  4699  nfco  4810  elrnmpt1  4896  nfimad  4997  iota2  5225  dffun4f  5251  nffun  5258  imadif  5315  funimaexglem  5318  nffn  5331  nff  5381  nff1  5438  nffo  5456  nff1o  5478  fun11iun  5501  nffvd  5546  fv3  5557  fmptco  5703  nfiso  5828  cbvriota  5862  riota2df  5872  riota5f  5876  nfoprab  5948  mpoeq123  5955  nfmpo  5965  cbvoprab1  5968  cbvoprab2  5969  cbvoprab12  5970  cbvoprab3  5972  cbvmpox  5974  ovmpodxf  6022  opabex3d  6146  opabex3  6147  dfoprab4f  6218  fmpox  6225  spc2ed  6258  cnvoprab  6259  f1od2  6260  opeliunxp2f  6263  nfrecs  6332  tfri3  6392  nffrec  6421  erovlem  6653  nfixpxy  6743  nfixp1  6744  xpf1o  6872  nneneq  6885  ac6sfi  6926  nfsup  7021  exmidomni  7170  fodjuomnilemdc  7172  ismkvnex  7183  mkvprop  7186  exmidfodomrlemr  7231  exmidfodomrlemrALT  7232  cc3  7297  caucvgsrlemgt1  7824  suplocsrlem  7837  axpre-suploclemres  7930  supinfneg  9625  infsupneg  9626  fimaxre2  11267  nfsum1  11396  nfsum  11397  fsumsplitf  11448  fsum2dlemstep  11474  fsum00  11502  nfcprod1  11594  nfcprod  11595  prodeq2  11597  fprod2dlemstep  11662  fprodsplitf  11672  fprodsplit1f  11674  fprodap0f  11676  fprodle  11680  zsupcllemstep  11978  bezoutlemmain  12031  bezoutlemzz  12035  bezout  12044  exmidunben  12477  ctiunctlemfo  12490  ctiunct  12491  mulcncf  14548  ellimc3apf  14586  limccnp2cntop  14603  bdsepnft  15097  bdsepnfALT  15099  bj-findis  15189  strcollnft  15194  strcollnfALT  15196  pw1nct  15211  isomninnlem  15237  trirec0  15251  iswomninnlem  15256  ismkvnnlem  15259