Theorem nfan 1579

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

Syntax hints:   ∧ wa 104  Ⅎwnf 1474

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 1461  ax-gen 1463  ax-4 1524

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

This theorem is referenced by:  nf3an  1580  cbvex2  1937  nfsbxyt  1962  nfsbv  1966  sbcomxyyz  1991  nfsb4t  2033  clelab  2322  nfel  2348  2ralbida  2518  r19.29an  2639  reean  2666  nfrabw  2678  cbvrexfw  2720  cbvrexf  2722  cbvreu  2727  cbvrab  2761  ceqsex2  2804  vtocl2gaf  2831  rspce  2863  eqvincf  2889  elrabf  2918  elrab3t  2919  rexab2  2930  morex  2948  reu2  2952  rmo3f  2961  sbc2iegf  3060  rmo2ilem  3079  rmo3  3081  csbiebt  3124  csbie2t  3133  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  nfopd  3826  eluniab  3852  dfnfc2  3858  nfdisjv  4023  disjiun  4029  nfopab  4102  cbvopab  4105  cbvopab1  4107  cbvopab2  4108  cbvopab1s  4109  mpteq12f  4114  nfmpt  4126  cbvmptf  4128  cbvmpt  4129  repizf2  4196  nfpo  4337  nfso  4338  nfwe  4391  onintonm  4554  peano2  4632  nfxp  4691  opeliunxp  4719  nfco  4832  elrnmpt1  4918  nfimad  5019  iota2  5249  dffun4f  5275  nffun  5282  imadif  5339  funimaexglem  5342  nffn  5355  nff  5405  nff1  5462  nffo  5480  nff1o  5503  fun11iun  5526  nffvd  5571  fv3  5582  fmptco  5729  nfiso  5854  cbvriota  5889  riota2df  5899  riota5f  5903  nfoprab  5975  mpoeq123  5982  nfmpo  5992  cbvoprab1  5995  cbvoprab2  5996  cbvoprab12  5997  cbvoprab3  5999  cbvmpox  6001  ovmpodxf  6049  elovmporab  6124  elovmporab1w  6125  opabex3d  6179  opabex3  6180  uchoice  6196  dfoprab4f  6252  fmpox  6259  spc2ed  6292  cnvoprab  6293  f1od2  6294  opeliunxp2f  6297  nfrecs  6366  tfri3  6426  nffrec  6455  erovlem  6687  nfixpxy  6777  nfixp1  6778  xpf1o  6906  nneneq  6919  ac6sfi  6960  opabfi  7000  nfsup  7059  exmidomni  7209  fodjuomnilemdc  7211  ismkvnex  7222  mkvprop  7225  exmidfodomrlemr  7271  exmidfodomrlemrALT  7272  cc3  7337  caucvgsrlemgt1  7864  suplocsrlem  7877  axpre-suploclemres  7970  supinfneg  9671  infsupneg  9672  zsupcllemstep  10321  nninfinf  10537  fimaxre2  11394  nfsum1  11523  nfsum  11524  fsumsplitf  11575  fsum2dlemstep  11601  fsum00  11629  nfcprod1  11721  nfcprod  11722  prodeq2  11724  fprod2dlemstep  11789  fprodsplitf  11799  fprodsplit1f  11801  fprodap0f  11803  fprodle  11807  bezoutlemmain  12175  bezoutlemzz  12179  bezout  12188  exmidunben  12653  ctiunctlemfo  12666  ctiunct  12667  mulcncf  14854  ellimc3apf  14906  limccnp2cntop  14923  bdsepnft  15543  bdsepnfALT  15545  bj-findis  15635  strcollnft  15640  strcollnfALT  15642  pw1nct  15657  isomninnlem  15684  trirec0  15698  iswomninnlem  15703  ismkvnnlem  15706