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  4199  cbvopab  4202  cbvopab1  4204  cbvopab2  4205  cbvopab1s  4206  mpteq12f  4211  nfmpt  4223  cbvmptf  4225  cbvmpt  4226  repizf2  4299  nfpo  4446  nfso  4447  nfwe  4500  onintonm  4664  peano2  4742  nfxp  4801  opeliunxp  4830  nfco  4945  elrnmpt1  5033  nfimad  5135  iota2  5367  dffun4f  5393  nffun  5400  imadif  5461  funimaexglem  5464  nffn  5477  nff  5530  nff1  5596  nffo  5614  nff1o  5637  fun11iun  5660  nffvd  5707  fv3  5718  fmptco  5874  nfiso  6012  cbvriota  6050  riota2df  6060  riota5f  6065  nfoprab  6140  mpoeq123  6147  nfmpo  6157  cbvoprab1  6160  cbvoprab2  6161  cbvoprab12  6162  cbvoprab3  6164  cbvmpox  6166  ovmpodxf  6214  elovmporab  6289  elovmporab1w  6290  opabex3d  6350  opabex3  6351  funimass4f  6359  uchoice  6371  dfoprab4f  6427  fmpox  6436  spc2ed  6469  cnvoprab  6470  f1od2  6471  opeliunxp2f  6509  nfrecs  6578  tfri3  6638  nffrec  6667  erovlem  6901  nfixpxy  6999  nfixp1  7000  modom  7108  xpf1o  7144  nneneq  7158  ac6sfi  7202  opabfi  7247  nfsup  7332  exmidomni  7482  fodjuomnilemdc  7484  ismkvnex  7495  mkvprop  7498  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  cc3  7634  caucvgsrlemgt1  8162  suplocsrlem  8175  axpre-suploclemres  8268  supinfneg  9997  infsupneg  9998  zsupcllemstep  10664  nninfinf  10882  reuccatpfxs1  11521  fimaxre2  11995  nfsum1  12124  nfsum  12125  fsumsplitf  12177  fsum2dlemstep  12203  fsum00  12231  nfcprod1  12323  nfcprod  12324  prodeq2  12326  fprod2dlemstep  12391  fprodsplitf  12401  fprodsplit1f  12403  fprodap0f  12405  fprodle  12409  bezoutlemmain  12777  bezoutlemzz  12781  bezout  12790  exmidunben  13319  ctiunctlemfo  13332  ctiunct  13333  mulcncf  15711  ellimc3apf  15763  limccnp2cntop  15780  bdsepnft  16925  bdsepnfALT  16927  bj-findis  17017  strcollnft  17022  strcollnfALT  17024  pw1nct  17045  isomninnlem  17091  trirec0  17105  iswomninnlem  17111  ismkvnnlem  17114  nfals  17156  nfrals  17157  nfalseu  17187  nfralseu  17188