Theorem nfan 1614

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

Syntax hints:   ∧ wa 104  Ⅎwnf 1509

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 1496  ax-gen 1498  ax-4 1559

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

This theorem is referenced by:  nf3an  1615  cbvex2  1972  nfsbxyt  1997  nfsbv  2001  sbcomxyyz  2026  nfsb4t  2068  clelab  2360  nfel  2393  2ralbida  2563  r19.29an  2685  reean  2712  nfrabw  2724  cbvrmow  2726  cbvrexfw  2767  cbvrexf  2769  cbvreu  2775  cbvrab  2810  ceqsex2  2854  vtocl2gaf  2881  rspce  2915  eqvincf  2941  elrabf  2970  elrab3t  2971  rexab2  2982  morex  3000  reu2  3004  rmo3f  3013  sbc2iegf  3112  reu8nf  3123  rmo2ilem  3132  rmo3  3134  csbiebt  3177  csbie2t  3186  cbvrexcsf  3201  cbvreucsf  3202  cbvrabcsf  3203  rabsnifsb  3756  nfopd  3899  eluniab  3925  dfnfc2  3931  nfdisjv  4096  disjiun  4103  nfopab  4177  cbvopab  4180  cbvopab1  4182  cbvopab2  4183  cbvopab1s  4184  mpteq12f  4189  nfmpt  4201  cbvmptf  4203  cbvmpt  4204  repizf2  4274  nfpo  4421  nfso  4422  nfwe  4475  onintonm  4638  peano2  4716  nfxp  4775  opeliunxp  4804  nfco  4919  elrnmpt1  5007  nfimad  5109  iota2  5341  dffun4f  5367  nffun  5374  imadif  5435  funimaexglem  5438  nffn  5451  nff  5504  nff1  5570  nffo  5588  nff1o  5611  fun11iun  5634  nffvd  5681  fv3  5692  fmptco  5842  nfiso  5978  cbvriota  6014  riota2df  6024  riota5f  6029  nfoprab  6104  mpoeq123  6111  nfmpo  6121  cbvoprab1  6124  cbvoprab2  6125  cbvoprab12  6126  cbvoprab3  6128  cbvmpox  6130  ovmpodxf  6178  elovmporab  6253  elovmporab1w  6254  opabex3d  6313  opabex3  6314  uchoice  6330  dfoprab4f  6386  fmpox  6395  spc2ed  6428  cnvoprab  6429  f1od2  6430  opeliunxp2f  6468  nfrecs  6537  tfri3  6597  nffrec  6626  erovlem  6860  nfixpxy  6951  nfixp1  6952  modom  7060  xpf1o  7096  nneneq  7110  ac6sfi  7154  opabfi  7199  nfsup  7282  exmidomni  7432  fodjuomnilemdc  7434  ismkvnex  7445  mkvprop  7448  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  cc3  7578  caucvgsrlemgt1  8106  suplocsrlem  8119  axpre-suploclemres  8212  supinfneg  9923  infsupneg  9924  zsupcllemstep  10585  nninfinf  10801  reuccatpfxs1  11432  fimaxre2  11905  nfsum1  12034  nfsum  12035  fsumsplitf  12087  fsum2dlemstep  12113  fsum00  12141  nfcprod1  12233  nfcprod  12234  prodeq2  12236  fprod2dlemstep  12301  fprodsplitf  12311  fprodsplit1f  12313  fprodap0f  12315  fprodle  12319  bezoutlemmain  12687  bezoutlemzz  12691  bezout  12700  exmidunben  13166  ctiunctlemfo  13179  ctiunct  13180  mulcncf  15460  ellimc3apf  15512  limccnp2cntop  15529  bdsepnft  16644  bdsepnfALT  16646  bj-findis  16736  strcollnft  16741  strcollnfALT  16743  pw1nct  16764  isomninnlem  16801  trirec0  16815  iswomninnlem  16821  ismkvnnlem  16824