Theorem nfan 1498

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

Syntax hints:   ∧ wa 102  Ⅎwnf 1390

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441

This theorem depends on definitions:  df-bi 115  df-nf 1391

This theorem is referenced by:  nf3an  1499  cbvex2  1840  nfsbxyt  1862  sbcomxyyz  1889  nfsb4t  1933  clelab  2207  nfel  2231  2ralbida  2393  reean  2528  nfrabxy  2540  cbvrexf  2578  cbvreu  2581  cbvrab  2610  ceqsex2  2650  vtocl2gaf  2676  rspce  2707  eqvincf  2730  elrabf  2757  elrab3t  2758  rexab2  2769  morex  2787  reu2  2791  sbc2iegf  2895  rmo2ilem  2914  rmo3  2916  csbiebt  2953  csbie2t  2961  cbvrexcsf  2976  cbvreucsf  2977  cbvrabcsf  2978  nfopd  3613  eluniab  3639  dfnfc2  3645  nfdisjv  3804  nfopab  3872  cbvopab  3875  cbvopab1  3877  cbvopab2  3878  cbvopab1s  3879  mpteq12f  3884  nfmpt  3896  cbvmpt  3898  repizf2  3962  nfpo  4092  nfso  4093  nfwe  4146  onintonm  4297  peano2  4373  nfxp  4427  opeliunxp  4451  nfco  4559  elrnmpt1  4644  nfimad  4738  iota2  4960  dffun4f  4985  nffun  4991  imadif  5047  funimaexglem  5050  nffn  5063  nff  5111  nff1  5162  nffo  5180  nff1o  5199  fun11iun  5222  nffvd  5262  fv3  5273  fmptco  5406  nfiso  5525  cbvriota  5557  riota2df  5567  riota5f  5571  nfoprab  5636  mpt2eq123  5643  nfmpt2  5652  cbvoprab1  5655  cbvoprab2  5656  cbvoprab12  5657  cbvoprab3  5659  cbvmpt2x  5661  ovmpt2dxf  5705  opabex3d  5827  opabex3  5828  dfoprab4f  5898  fmpt2x  5905  spc2ed  5933  cnvoprab  5934  f1od2  5935  nfrecs  6004  tfri3  6064  nffrec  6093  erovlem  6314  xpf1o  6490  nneneq  6503  ac6sfi  6544  nfsup  6594  exmidomni  6703  fodjuomnilemdc  6704  exmidfodomrlemr  6731  exmidfodomrlemrALT  6732  caucvgsrlemgt1  7243  supinfneg  8978  infsupneg  8979  fimaxre2  10483  nfsum1  10567  nfsum  10568  zsupcllemstep  10721  bezoutlemmain  10767  bezoutlemzz  10771  bezout  10780  bdsepnft  11121  bdsepnfALT  11123  bj-findis  11217  strcollnft  11222