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

Syntax hints:   ∧ wa 104  Ⅎwnf 1513

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 1500  ax-gen 1502  ax-4 1563

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

This theorem is referenced 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  3776  nfopd  3919  eluniab  3945  dfnfc2  3951  nfdisjv  4116  disjiun  4123  nfopab  4197  cbvopab  4200  cbvopab1  4202  cbvopab2  4203  cbvopab1s  4204  mpteq12f  4209  nfmpt  4221  cbvmptf  4223  cbvmpt  4224  repizf2  4297  nfpo  4444  nfso  4445  nfwe  4498  onintonm  4662  peano2  4740  nfxp  4799  opeliunxp  4828  nfco  4943  elrnmpt1  5031  nfimad  5133  iota2  5365  dffun4f  5391  nffun  5398  imadif  5459  funimaexglem  5462  nffn  5475  nff  5528  nff1  5594  nffo  5612  nff1o  5635  fun11iun  5658  nffvd  5705  fv3  5716  fmptco  5868  nfiso  6006  cbvriota  6044  riota2df  6054  riota5f  6059  nfoprab  6134  mpoeq123  6141  nfmpo  6151  cbvoprab1  6154  cbvoprab2  6155  cbvoprab12  6156  cbvoprab3  6158  cbvmpox  6160  ovmpodxf  6208  elovmporab  6283  elovmporab1w  6284  opabex3d  6344  opabex3  6345  funimass4f  6353  uchoice  6365  dfoprab4f  6421  fmpox  6430  spc2ed  6463  cnvoprab  6464  f1od2  6465  opeliunxp2f  6503  nfrecs  6572  tfri3  6632  nffrec  6661  erovlem  6895  nfixpxy  6993  nfixp1  6994  modom  7102  xpf1o  7138  nneneq  7152  ac6sfi  7196  opabfi  7241  nfsup  7326  exmidomni  7476  fodjuomnilemdc  7478  ismkvnex  7489  mkvprop  7492  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  cc3  7628  caucvgsrlemgt1  8156  suplocsrlem  8169  axpre-suploclemres  8262  supinfneg  9978  infsupneg  9979  zsupcllemstep  10645  nninfinf  10863  reuccatpfxs1  11502  fimaxre2  11976  nfsum1  12105  nfsum  12106  fsumsplitf  12158  fsum2dlemstep  12184  fsum00  12212  nfcprod1  12304  nfcprod  12305  prodeq2  12307  fprod2dlemstep  12372  fprodsplitf  12382  fprodsplit1f  12384  fprodap0f  12386  fprodle  12390  bezoutlemmain  12758  bezoutlemzz  12762  bezout  12771  exmidunben  13300  ctiunctlemfo  13313  ctiunct  13314  mulcncf  15692  ellimc3apf  15744  limccnp2cntop  15761  bdsepnft  16896  bdsepnfALT  16898  bj-findis  16988  strcollnft  16993  strcollnfALT  16995  pw1nct  17016  isomninnlem  17053  trirec0  17067  iswomninnlem  17073  ismkvnnlem  17076  nfals  17118  nfrals  17119