Theorem nfan 1613

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

Syntax hints:   ∧ wa 104  Ⅎwnf 1508

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 1495  ax-gen 1497  ax-4 1558

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

This theorem is referenced by:  nf3an  1614  cbvex2  1970  nfsbxyt  1995  nfsbv  1999  sbcomxyyz  2024  nfsb4t  2066  clelab  2356  nfel  2382  2ralbida  2552  r19.29an  2674  reean  2701  nfrabw  2713  cbvrmow  2715  cbvrexfw  2756  cbvrexf  2758  cbvreu  2764  cbvrab  2799  ceqsex2  2843  vtocl2gaf  2870  rspce  2904  eqvincf  2930  elrabf  2959  elrab3t  2960  rexab2  2971  morex  2989  reu2  2993  rmo3f  3002  sbc2iegf  3101  reu8nf  3112  rmo2ilem  3121  rmo3  3123  csbiebt  3166  csbie2t  3175  cbvrexcsf  3190  cbvreucsf  3191  cbvrabcsf  3192  rabsnifsb  3738  nfopd  3880  eluniab  3906  dfnfc2  3912  nfdisjv  4077  disjiun  4084  nfopab  4158  cbvopab  4161  cbvopab1  4163  cbvopab2  4164  cbvopab1s  4165  mpteq12f  4170  nfmpt  4182  cbvmptf  4184  cbvmpt  4185  repizf2  4254  nfpo  4400  nfso  4401  nfwe  4454  onintonm  4617  peano2  4695  nfxp  4754  opeliunxp  4783  nfco  4897  elrnmpt1  4985  nfimad  5087  iota2  5318  dffun4f  5344  nffun  5351  imadif  5412  funimaexglem  5415  nffn  5428  nff  5481  nff1  5543  nffo  5561  nff1o  5584  fun11iun  5607  nffvd  5654  fv3  5665  fmptco  5816  nfiso  5952  cbvriota  5988  riota2df  5998  riota5f  6003  nfoprab  6078  mpoeq123  6085  nfmpo  6095  cbvoprab1  6098  cbvoprab2  6099  cbvoprab12  6100  cbvoprab3  6102  cbvmpox  6104  ovmpodxf  6152  elovmporab  6227  elovmporab1w  6228  opabex3d  6288  opabex3  6289  uchoice  6305  dfoprab4f  6361  fmpox  6370  spc2ed  6403  cnvoprab  6404  f1od2  6405  opeliunxp2f  6409  nfrecs  6478  tfri3  6538  nffrec  6567  erovlem  6801  nfixpxy  6891  nfixp1  6892  modom  6999  xpf1o  7035  nneneq  7048  ac6sfi  7092  opabfi  7137  nfsup  7196  exmidomni  7346  fodjuomnilemdc  7348  ismkvnex  7359  mkvprop  7362  exmidfodomrlemr  7418  exmidfodomrlemrALT  7419  cc3  7492  caucvgsrlemgt1  8020  suplocsrlem  8033  axpre-suploclemres  8126  supinfneg  9834  infsupneg  9835  zsupcllemstep  10495  nninfinf  10711  reuccatpfxs1  11337  fimaxre2  11810  nfsum1  11939  nfsum  11940  fsumsplitf  11992  fsum2dlemstep  12018  fsum00  12046  nfcprod1  12138  nfcprod  12139  prodeq2  12141  fprod2dlemstep  12206  fprodsplitf  12216  fprodsplit1f  12218  fprodap0f  12220  fprodle  12224  bezoutlemmain  12592  bezoutlemzz  12596  bezout  12605  exmidunben  13070  ctiunctlemfo  13083  ctiunct  13084  mulcncf  15361  ellimc3apf  15413  limccnp2cntop  15430  bdsepnft  16542  bdsepnfALT  16544  bj-findis  16634  strcollnft  16639  strcollnfALT  16641  pw1nct  16664  isomninnlem  16701  trirec0  16715  iswomninnlem  16721  ismkvnnlem  16724