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  2797  ceqsex2  2841  vtocl2gaf  2868  rspce  2902  eqvincf  2928  elrabf  2957  elrab3t  2958  rexab2  2969  morex  2987  reu2  2991  rmo3f  3000  sbc2iegf  3099  reu8nf  3110  rmo2ilem  3119  rmo3  3121  csbiebt  3164  csbie2t  3173  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  nfopd  3874  eluniab  3900  dfnfc2  3906  nfdisjv  4071  disjiun  4078  nfopab  4152  cbvopab  4155  cbvopab1  4157  cbvopab2  4158  cbvopab1s  4159  mpteq12f  4164  nfmpt  4176  cbvmptf  4178  cbvmpt  4179  repizf2  4246  nfpo  4392  nfso  4393  nfwe  4446  onintonm  4609  peano2  4687  nfxp  4746  opeliunxp  4774  nfco  4887  elrnmpt1  4975  nfimad  5077  iota2  5308  dffun4f  5334  nffun  5341  imadif  5401  funimaexglem  5404  nffn  5417  nff  5470  nff1  5531  nffo  5549  nff1o  5572  fun11iun  5595  nffvd  5641  fv3  5652  fmptco  5803  nfiso  5936  cbvriota  5972  riota2df  5982  riota5f  5987  nfoprab  6062  mpoeq123  6069  nfmpo  6079  cbvoprab1  6082  cbvoprab2  6083  cbvoprab12  6084  cbvoprab3  6086  cbvmpox  6088  ovmpodxf  6136  elovmporab  6211  elovmporab1w  6212  opabex3d  6272  opabex3  6273  uchoice  6289  dfoprab4f  6345  fmpox  6352  spc2ed  6385  cnvoprab  6386  f1od2  6387  opeliunxp2f  6390  nfrecs  6459  tfri3  6519  nffrec  6548  erovlem  6782  nfixpxy  6872  nfixp1  6873  xpf1o  7013  nneneq  7026  ac6sfi  7068  opabfi  7108  nfsup  7167  exmidomni  7317  fodjuomnilemdc  7319  ismkvnex  7330  mkvprop  7333  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  cc3  7462  caucvgsrlemgt1  7990  suplocsrlem  8003  axpre-suploclemres  8096  supinfneg  9798  infsupneg  9799  zsupcllemstep  10457  nninfinf  10673  reuccatpfxs1  11287  fimaxre2  11746  nfsum1  11875  nfsum  11876  fsumsplitf  11927  fsum2dlemstep  11953  fsum00  11981  nfcprod1  12073  nfcprod  12074  prodeq2  12076  fprod2dlemstep  12141  fprodsplitf  12151  fprodsplit1f  12153  fprodap0f  12155  fprodle  12159  bezoutlemmain  12527  bezoutlemzz  12531  bezout  12540  exmidunben  13005  ctiunctlemfo  13018  ctiunct  13019  mulcncf  15290  ellimc3apf  15342  limccnp2cntop  15359  bdsepnft  16274  bdsepnfALT  16276  bj-findis  16366  strcollnft  16371  strcollnfALT  16373  pw1nct  16398  isomninnlem  16428  trirec0  16442  iswomninnlem  16447  ismkvnnlem  16450