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  5407  nff1  5464  nffo  5482  nff1o  5505  fun11iun  5528  nffvd  5573  fv3  5584  fmptco  5731  nfiso  5856  cbvriota  5891  riota2df  5901  riota5f  5905  nfoprab  5978  mpoeq123  5985  nfmpo  5995  cbvoprab1  5998  cbvoprab2  5999  cbvoprab12  6000  cbvoprab3  6002  cbvmpox  6004  ovmpodxf  6052  elovmporab  6127  elovmporab1w  6128  opabex3d  6187  opabex3  6188  uchoice  6204  dfoprab4f  6260  fmpox  6267  spc2ed  6300  cnvoprab  6301  f1od2  6302  opeliunxp2f  6305  nfrecs  6374  tfri3  6434  nffrec  6463  erovlem  6695  nfixpxy  6785  nfixp1  6786  xpf1o  6914  nneneq  6927  ac6sfi  6968  opabfi  7008  nfsup  7067  exmidomni  7217  fodjuomnilemdc  7219  ismkvnex  7230  mkvprop  7233  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  cc3  7353  caucvgsrlemgt1  7881  suplocsrlem  7894  axpre-suploclemres  7987  supinfneg  9688  infsupneg  9689  zsupcllemstep  10338  nninfinf  10554  fimaxre2  11411  nfsum1  11540  nfsum  11541  fsumsplitf  11592  fsum2dlemstep  11618  fsum00  11646  nfcprod1  11738  nfcprod  11739  prodeq2  11741  fprod2dlemstep  11806  fprodsplitf  11816  fprodsplit1f  11818  fprodap0f  11820  fprodle  11824  bezoutlemmain  12192  bezoutlemzz  12196  bezout  12205  exmidunben  12670  ctiunctlemfo  12683  ctiunct  12684  mulcncf  14930  ellimc3apf  14982  limccnp2cntop  14999  bdsepnft  15619  bdsepnfALT  15621  bj-findis  15711  strcollnft  15716  strcollnfALT  15718  pw1nct  15736  isomninnlem  15765  trirec0  15779  iswomninnlem  15784  ismkvnnlem  15787