Theorem nfan 1614

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

Syntax hints:   ∧ wa 104  Ⅎwnf 1509

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 1496  ax-gen 1498  ax-4 1559

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

This theorem is referenced by:  nf3an  1615  cbvex2  1974  nfsbxyt  1999  nfsbv  2003  sbcomxyyz  2028  nfsb4t  2070  clelab  2362  nfel  2395  2ralbida  2565  r19.29an  2687  reean  2714  nfrabw  2727  cbvrmow  2729  cbvrexfw  2770  cbvrexf  2772  cbvreu  2778  cbvrab  2813  ceqsex2  2857  vtocl2gaf  2884  rspce  2918  eqvincf  2945  elrabf  2974  elrab3t  2975  rexab2  2986  morex  3004  reu2  3008  rmo3f  3017  sbc2iegf  3116  reu8nf  3127  rmo2ilem  3136  rmo3  3138  csbiebt  3181  csbie2t  3190  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  rabsnifsb  3762  nfopd  3905  eluniab  3931  dfnfc2  3937  nfdisjv  4102  disjiun  4109  nfopab  4183  cbvopab  4186  cbvopab1  4188  cbvopab2  4189  cbvopab1s  4190  mpteq12f  4195  nfmpt  4207  cbvmptf  4209  cbvmpt  4210  repizf2  4280  nfpo  4427  nfso  4428  nfwe  4481  onintonm  4644  peano2  4722  nfxp  4781  opeliunxp  4810  nfco  4925  elrnmpt1  5013  nfimad  5115  iota2  5347  dffun4f  5373  nffun  5380  imadif  5441  funimaexglem  5444  nffn  5457  nff  5510  nff1  5576  nffo  5594  nff1o  5617  fun11iun  5640  nffvd  5687  fv3  5698  fmptco  5848  nfiso  5985  cbvriota  6023  riota2df  6033  riota5f  6038  nfoprab  6113  mpoeq123  6120  nfmpo  6130  cbvoprab1  6133  cbvoprab2  6134  cbvoprab12  6135  cbvoprab3  6137  cbvmpox  6139  ovmpodxf  6187  elovmporab  6262  elovmporab1w  6263  opabex3d  6323  opabex3  6324  funimass4f  6332  uchoice  6344  dfoprab4f  6400  fmpox  6409  spc2ed  6442  cnvoprab  6443  f1od2  6444  opeliunxp2f  6482  nfrecs  6551  tfri3  6611  nffrec  6640  erovlem  6874  nfixpxy  6965  nfixp1  6966  modom  7074  xpf1o  7110  nneneq  7124  ac6sfi  7168  opabfi  7213  nfsup  7296  exmidomni  7446  fodjuomnilemdc  7448  ismkvnex  7459  mkvprop  7462  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  cc3  7598  caucvgsrlemgt1  8126  suplocsrlem  8139  axpre-suploclemres  8232  supinfneg  9948  infsupneg  9949  zsupcllemstep  10614  nninfinf  10832  reuccatpfxs1  11467  fimaxre2  11940  nfsum1  12069  nfsum  12070  fsumsplitf  12122  fsum2dlemstep  12148  fsum00  12176  nfcprod1  12268  nfcprod  12269  prodeq2  12271  fprod2dlemstep  12336  fprodsplitf  12346  fprodsplit1f  12348  fprodap0f  12350  fprodle  12354  bezoutlemmain  12722  bezoutlemzz  12726  bezout  12735  exmidunben  13264  ctiunctlemfo  13277  ctiunct  13278  mulcncf  15602  ellimc3apf  15654  limccnp2cntop  15671  bdsepnft  16796  bdsepnfALT  16798  bj-findis  16888  strcollnft  16893  strcollnfALT  16895  pw1nct  16916  isomninnlem  16953  trirec0  16967  iswomninnlem  16973  ismkvnnlem  16976