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  4247  nfpo  4393  nfso  4394  nfwe  4447  onintonm  4610  peano2  4688  nfxp  4747  opeliunxp  4776  nfco  4890  elrnmpt1  4978  nfimad  5080  iota2  5311  dffun4f  5337  nffun  5344  imadif  5404  funimaexglem  5407  nffn  5420  nff  5473  nff1  5534  nffo  5552  nff1o  5575  fun11iun  5598  nffvd  5644  fv3  5655  fmptco  5806  nfiso  5939  cbvriota  5975  riota2df  5985  riota5f  5990  nfoprab  6065  mpoeq123  6072  nfmpo  6082  cbvoprab1  6085  cbvoprab2  6086  cbvoprab12  6087  cbvoprab3  6089  cbvmpox  6091  ovmpodxf  6139  elovmporab  6214  elovmporab1w  6215  opabex3d  6275  opabex3  6276  uchoice  6292  dfoprab4f  6348  fmpox  6357  spc2ed  6390  cnvoprab  6391  f1od2  6392  opeliunxp2f  6395  nfrecs  6464  tfri3  6524  nffrec  6553  erovlem  6787  nfixpxy  6877  nfixp1  6878  xpf1o  7018  nneneq  7031  ac6sfi  7073  opabfi  7116  nfsup  7175  exmidomni  7325  fodjuomnilemdc  7327  ismkvnex  7338  mkvprop  7341  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  cc3  7470  caucvgsrlemgt1  7998  suplocsrlem  8011  axpre-suploclemres  8104  supinfneg  9807  infsupneg  9808  zsupcllemstep  10466  nninfinf  10682  reuccatpfxs1  11300  fimaxre2  11759  nfsum1  11888  nfsum  11889  fsumsplitf  11940  fsum2dlemstep  11966  fsum00  11994  nfcprod1  12086  nfcprod  12087  prodeq2  12089  fprod2dlemstep  12154  fprodsplitf  12164  fprodsplit1f  12166  fprodap0f  12168  fprodle  12172  bezoutlemmain  12540  bezoutlemzz  12544  bezout  12553  exmidunben  13018  ctiunctlemfo  13031  ctiunct  13032  mulcncf  15303  ellimc3apf  15355  limccnp2cntop  15372  bdsepnft  16359  bdsepnfALT  16361  bj-findis  16451  strcollnft  16456  strcollnfALT  16458  pw1nct  16482  isomninnlem  16512  trirec0  16526  iswomninnlem  16531  ismkvnnlem  16534