Theorem nfan 1565

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

Syntax hints:   ∧ wa 104  Ⅎwnf 1460

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 1447  ax-gen 1449  ax-4 1510

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

This theorem is referenced by:  nf3an  1566  cbvex2  1922  nfsbxyt  1943  nfsbv  1947  sbcomxyyz  1972  nfsb4t  2014  clelab  2303  nfel  2328  2ralbida  2498  r19.29an  2619  reean  2646  nfrabxy  2658  cbvrexfw  2696  cbvrexf  2698  cbvreu  2703  cbvrab  2737  ceqsex2  2779  vtocl2gaf  2806  rspce  2838  eqvincf  2864  elrabf  2893  elrab3t  2894  rexab2  2905  morex  2923  reu2  2927  rmo3f  2936  sbc2iegf  3035  rmo2ilem  3054  rmo3  3056  csbiebt  3098  csbie2t  3107  cbvrexcsf  3122  cbvreucsf  3123  cbvrabcsf  3124  nfopd  3797  eluniab  3823  dfnfc2  3829  nfdisjv  3994  disjiun  4000  nfopab  4073  cbvopab  4076  cbvopab1  4078  cbvopab2  4079  cbvopab1s  4080  mpteq12f  4085  nfmpt  4097  cbvmptf  4099  cbvmpt  4100  repizf2  4164  nfpo  4303  nfso  4304  nfwe  4357  onintonm  4518  peano2  4596  nfxp  4655  opeliunxp  4683  nfco  4794  elrnmpt1  4880  nfimad  4981  iota2  5208  dffun4f  5234  nffun  5241  imadif  5298  funimaexglem  5301  nffn  5314  nff  5364  nff1  5421  nffo  5439  nff1o  5461  fun11iun  5484  nffvd  5529  fv3  5540  fmptco  5684  nfiso  5809  cbvriota  5843  riota2df  5853  riota5f  5857  nfoprab  5929  mpoeq123  5936  nfmpo  5946  cbvoprab1  5949  cbvoprab2  5950  cbvoprab12  5951  cbvoprab3  5953  cbvmpox  5955  ovmpodxf  6002  opabex3d  6124  opabex3  6125  dfoprab4f  6196  fmpox  6203  spc2ed  6236  cnvoprab  6237  f1od2  6238  opeliunxp2f  6241  nfrecs  6310  tfri3  6370  nffrec  6399  erovlem  6629  nfixpxy  6719  nfixp1  6720  xpf1o  6846  nneneq  6859  ac6sfi  6900  nfsup  6993  exmidomni  7142  fodjuomnilemdc  7144  ismkvnex  7155  mkvprop  7158  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  cc3  7269  caucvgsrlemgt1  7796  suplocsrlem  7809  axpre-suploclemres  7902  supinfneg  9597  infsupneg  9598  fimaxre2  11237  nfsum1  11366  nfsum  11367  fsumsplitf  11418  fsum2dlemstep  11444  fsum00  11472  nfcprod1  11564  nfcprod  11565  prodeq2  11567  fprod2dlemstep  11632  fprodsplitf  11642  fprodsplit1f  11644  fprodap0f  11646  fprodle  11650  zsupcllemstep  11948  bezoutlemmain  12001  bezoutlemzz  12005  bezout  12014  exmidunben  12429  ctiunctlemfo  12442  ctiunct  12443  mulcncf  14130  ellimc3apf  14168  limccnp2cntop  14185  bdsepnft  14678  bdsepnfALT  14680  bj-findis  14770  strcollnft  14775  strcollnfALT  14777  pw1nct  14791  isomninnlem  14817  trirec0  14831  iswomninnlem  14836  ismkvnnlem  14839