Theorem nfan 1618

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 1617	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

This proof depends on syntax axioms:   ∧ wa 104  Ⅎwnf 1513

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563

This proof depends on definitions:  df-bi 117  df-nf 1514

This theorem is used by:  nf3an  1619  cbvex2  1978  nfsbxyt  2003  nfsbv  2007  sbcomxyyz  2032  nfsb4t  2074  clelab  2366  nfel  2401  2ralbida  2571  r19.29an  2693  reean  2720  nfrabw  2733  cbvrmow  2735  cbvrexfw  2776  cbvrexf  2778  cbvreu  2784  cbvrab  2819  ceqsex2  2863  vtocl2gaf  2890  rspce  2924  eqvincf  2951  elrabf  2980  elrab3t  2981  rexab2  2992  morex  3010  reu2  3014  rmo3f  3023  sbc2iegf  3122  reu8nf  3133  rmo2ilem  3142  rmo3  3144  csbiebt  3187  csbie2t  3196  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  rabsnifsb  3777  nfopd  3921  eluniab  3947  dfnfc2  3953  nfdisjv  4118  disjiun  4125  nfopab  4200  cbvopab  4203  cbvopab1  4205  cbvopab2  4206  cbvopab1s  4207  mpteq12f  4212  nfmpt  4225  cbvmptf  4227  cbvmpt  4228  repizf2  4301  nfpo  4448  nfso  4449  nfwe  4502  onintonm  4666  peano2  4744  nfxp  4803  opeliunxp  4832  nfco  4947  elrnmpt1  5035  nfimad  5138  iota2  5370  dffun4f  5396  nffun  5403  imadif  5464  funimaexglem  5467  nffn  5480  nff  5533  nff1  5599  nffo  5617  nff1o  5640  fun11iun  5663  nffvd  5710  fv3  5721  fmptco  5877  nfiso  6015  cbvriota  6053  riota2df  6063  riota5f  6068  nfoprab  6143  mpoeq123  6150  nfmpo  6160  cbvoprab1  6163  cbvoprab2  6164  cbvoprab12  6165  cbvoprab3  6167  cbvmpox  6169  ovmpodxf  6217  elovmporab  6292  elovmporab1w  6293  opabex3d  6354  opabex3  6355  funimass4f  6363  uchoice  6375  dfoprab4f  6431  fmpox  6440  spc2ed  6473  cnvoprab  6474  f1od2  6475  opeliunxp2f  6513  nfrecs  6582  tfri3  6642  nffrec  6671  erovlem  6905  nfixpxy  7004  nfixp1  7005  modom  7113  xpf1o  7149  nneneq  7163  ac6sfi  7207  opabfi  7252  nfsup  7339  exmidomni  7489  fodjuomnilemdc  7491  ismkvnex  7502  mkvprop  7505  exmidfodomrlemr  7561  exmidfodomrlemrALT  7562  cc3  7641  caucvgsrlemgt1  8169  suplocsrlem  8182  axpre-suploclemres  8275  supinfneg  10012  infsupneg  10013  zsupcllemstep  10680  nninfinf  10902  reuccatpfxs1  11542  fimaxre2  12017  nfsum1  12148  nfsum  12149  fsumsplitf  12201  fsum2dlemstep  12227  fsum00  12255  nfcprod1  12347  nfcprod  12348  prodeq2  12350  fprod2dlemstep  12415  fprodsplitf  12425  fprodsplit1f  12427  fprodap0f  12429  fprodle  12433  bezoutlemmain  12801  bezoutlemzz  12805  bezout  12814  exmidunben  13376  ctiunctlemfo  13389  ctiunct  13390  gsumsnfdcmn  14258  mulcncf  15846  ellimc3apf  15898  limccnp2cntop  15915  bdsepnft  17130  bdsepnfALT  17132  bj-findis  17222  strcollnft  17227  strcollnfALT  17229  pw1nct  17250  isomninnlem  17297  trirec0  17312  iswomninnlem  17318  ismkvnnlem  17321  nfals  17363  nfrals  17364  nfalseu  17394  nfralseu  17395