Theorem nfan 1611

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

Syntax hints:   ∧ wa 104  Ⅎwnf 1506

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 1493  ax-gen 1495  ax-4 1556

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

This theorem is referenced by:  nf3an  1612  cbvex2  1969  nfsbxyt  1994  nfsbv  1998  sbcomxyyz  2023  nfsb4t  2065  clelab  2355  nfel  2381  2ralbida  2551  r19.29an  2673  reean  2700  nfrabw  2712  cbvrmow  2714  cbvrexfw  2755  cbvrexf  2757  cbvreu  2763  cbvrab  2798  ceqsex2  2842  vtocl2gaf  2869  rspce  2903  eqvincf  2929  elrabf  2958  elrab3t  2959  rexab2  2970  morex  2988  reu2  2992  rmo3f  3001  sbc2iegf  3100  reu8nf  3111  rmo2ilem  3120  rmo3  3122  csbiebt  3165  csbie2t  3174  cbvrexcsf  3189  cbvreucsf  3190  cbvrabcsf  3191  rabsnifsb  3735  nfopd  3877  eluniab  3903  dfnfc2  3909  nfdisjv  4074  disjiun  4081  nfopab  4155  cbvopab  4158  cbvopab1  4160  cbvopab2  4161  cbvopab1s  4162  mpteq12f  4167  nfmpt  4179  cbvmptf  4181  cbvmpt  4182  repizf2  4250  nfpo  4396  nfso  4397  nfwe  4450  onintonm  4613  peano2  4691  nfxp  4750  opeliunxp  4779  nfco  4893  elrnmpt1  4981  nfimad  5083  iota2  5314  dffun4f  5340  nffun  5347  imadif  5407  funimaexglem  5410  nffn  5423  nff  5476  nff1  5537  nffo  5555  nff1o  5578  fun11iun  5601  nffvd  5647  fv3  5658  fmptco  5809  nfiso  5942  cbvriota  5978  riota2df  5988  riota5f  5993  nfoprab  6068  mpoeq123  6075  nfmpo  6085  cbvoprab1  6088  cbvoprab2  6089  cbvoprab12  6090  cbvoprab3  6092  cbvmpox  6094  ovmpodxf  6142  elovmporab  6217  elovmporab1w  6218  opabex3d  6278  opabex3  6279  uchoice  6295  dfoprab4f  6351  fmpox  6360  spc2ed  6393  cnvoprab  6394  f1od2  6395  opeliunxp2f  6399  nfrecs  6468  tfri3  6528  nffrec  6557  erovlem  6791  nfixpxy  6881  nfixp1  6882  modom  6989  xpf1o  7025  nneneq  7038  ac6sfi  7082  opabfi  7126  nfsup  7185  exmidomni  7335  fodjuomnilemdc  7337  ismkvnex  7348  mkvprop  7351  exmidfodomrlemr  7406  exmidfodomrlemrALT  7407  cc3  7480  caucvgsrlemgt1  8008  suplocsrlem  8021  axpre-suploclemres  8114  supinfneg  9822  infsupneg  9823  zsupcllemstep  10482  nninfinf  10698  reuccatpfxs1  11321  fimaxre2  11781  nfsum1  11910  nfsum  11911  fsumsplitf  11962  fsum2dlemstep  11988  fsum00  12016  nfcprod1  12108  nfcprod  12109  prodeq2  12111  fprod2dlemstep  12176  fprodsplitf  12186  fprodsplit1f  12188  fprodap0f  12190  fprodle  12194  bezoutlemmain  12562  bezoutlemzz  12566  bezout  12575  exmidunben  13040  ctiunctlemfo  13053  ctiunct  13054  mulcncf  15325  ellimc3apf  15377  limccnp2cntop  15394  bdsepnft  16432  bdsepnfALT  16434  bj-findis  16524  strcollnft  16529  strcollnfALT  16531  pw1nct  16554  isomninnlem  16584  trirec0  16598  iswomninnlem  16603  ismkvnnlem  16606