Theorem nfan 1591

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

Syntax hints:   ∧ wa 104  Ⅎwnf 1486

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 1473  ax-gen 1475  ax-4 1536

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

This theorem is referenced by:  nf3an  1592  cbvex2  1949  nfsbxyt  1974  nfsbv  1978  sbcomxyyz  2003  nfsb4t  2045  clelab  2335  nfel  2361  2ralbida  2531  r19.29an  2653  reean  2680  nfrabw  2692  cbvrmow  2694  cbvrexfw  2735  cbvrexf  2737  cbvreu  2743  cbvrab  2777  ceqsex2  2821  vtocl2gaf  2848  rspce  2882  eqvincf  2908  elrabf  2937  elrab3t  2938  rexab2  2949  morex  2967  reu2  2971  rmo3f  2980  sbc2iegf  3079  reu8nf  3090  rmo2ilem  3099  rmo3  3101  csbiebt  3144  csbie2t  3153  cbvrexcsf  3168  cbvreucsf  3169  cbvrabcsf  3170  nfopd  3853  eluniab  3879  dfnfc2  3885  nfdisjv  4050  disjiun  4057  nfopab  4131  cbvopab  4134  cbvopab1  4136  cbvopab2  4137  cbvopab1s  4138  mpteq12f  4143  nfmpt  4155  cbvmptf  4157  cbvmpt  4158  repizf2  4225  nfpo  4369  nfso  4370  nfwe  4423  onintonm  4586  peano2  4664  nfxp  4723  opeliunxp  4751  nfco  4864  elrnmpt1  4951  nfimad  5053  iota2  5284  dffun4f  5310  nffun  5317  imadif  5377  funimaexglem  5380  nffn  5393  nff  5446  nff1  5505  nffo  5523  nff1o  5546  fun11iun  5569  nffvd  5615  fv3  5626  fmptco  5774  nfiso  5903  cbvriota  5939  riota2df  5949  riota5f  5954  nfoprab  6027  mpoeq123  6034  nfmpo  6044  cbvoprab1  6047  cbvoprab2  6048  cbvoprab12  6049  cbvoprab3  6051  cbvmpox  6053  ovmpodxf  6101  elovmporab  6176  elovmporab1w  6177  opabex3d  6236  opabex3  6237  uchoice  6253  dfoprab4f  6309  fmpox  6316  spc2ed  6349  cnvoprab  6350  f1od2  6351  opeliunxp2f  6354  nfrecs  6423  tfri3  6483  nffrec  6512  erovlem  6744  nfixpxy  6834  nfixp1  6835  xpf1o  6973  nneneq  6986  ac6sfi  7028  opabfi  7068  nfsup  7127  exmidomni  7277  fodjuomnilemdc  7279  ismkvnex  7290  mkvprop  7293  exmidfodomrlemr  7348  exmidfodomrlemrALT  7349  cc3  7422  caucvgsrlemgt1  7950  suplocsrlem  7963  axpre-suploclemres  8056  supinfneg  9758  infsupneg  9759  zsupcllemstep  10416  nninfinf  10632  reuccatpfxs1  11245  fimaxre2  11704  nfsum1  11833  nfsum  11834  fsumsplitf  11885  fsum2dlemstep  11911  fsum00  11939  nfcprod1  12031  nfcprod  12032  prodeq2  12034  fprod2dlemstep  12099  fprodsplitf  12109  fprodsplit1f  12111  fprodap0f  12113  fprodle  12117  bezoutlemmain  12485  bezoutlemzz  12489  bezout  12498  exmidunben  12963  ctiunctlemfo  12976  ctiunct  12977  mulcncf  15247  ellimc3apf  15299  limccnp2cntop  15316  bdsepnft  16160  bdsepnfALT  16162  bj-findis  16252  strcollnft  16257  strcollnfALT  16259  pw1nct  16280  isomninnlem  16309  trirec0  16323  iswomninnlem  16328  ismkvnnlem  16331