Theorem nfan 1545

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

Syntax hints:   ∧ wa 103  Ⅎwnf 1437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488

This theorem depends on definitions:  df-bi 116  df-nf 1438

This theorem is referenced by:  nf3an  1546  cbvex2  1895  nfsbxyt  1917  sbcomxyyz  1946  nfsb4t  1990  clelab  2266  nfel  2291  2ralbida  2459  r19.29an  2577  reean  2602  nfrabxy  2614  cbvrexf  2652  cbvreu  2655  cbvrab  2687  ceqsex2  2729  vtocl2gaf  2756  rspce  2788  eqvincf  2814  elrabf  2842  elrab3t  2843  rexab2  2854  morex  2872  reu2  2876  rmo3f  2885  sbc2iegf  2983  rmo2ilem  3002  rmo3  3004  csbiebt  3044  csbie2t  3053  cbvrexcsf  3068  cbvreucsf  3069  cbvrabcsf  3070  nfopd  3730  eluniab  3756  dfnfc2  3762  nfdisjv  3926  disjiun  3932  nfopab  4004  cbvopab  4007  cbvopab1  4009  cbvopab2  4010  cbvopab1s  4011  mpteq12f  4016  nfmpt  4028  cbvmptf  4030  cbvmpt  4031  repizf2  4094  nfpo  4231  nfso  4232  nfwe  4285  onintonm  4441  peano2  4517  nfxp  4574  opeliunxp  4602  nfco  4712  elrnmpt1  4798  nfimad  4898  iota2  5122  dffun4f  5147  nffun  5154  imadif  5211  funimaexglem  5214  nffn  5227  nff  5277  nff1  5334  nffo  5352  nff1o  5373  fun11iun  5396  nffvd  5441  fv3  5452  fmptco  5594  nfiso  5715  cbvriota  5748  riota2df  5758  riota5f  5762  nfoprab  5831  mpoeq123  5838  nfmpo  5848  cbvoprab1  5851  cbvoprab2  5852  cbvoprab12  5853  cbvoprab3  5855  cbvmpox  5857  ovmpodxf  5904  opabex3d  6027  opabex3  6028  dfoprab4f  6099  fmpox  6106  spc2ed  6138  cnvoprab  6139  f1od2  6140  opeliunxp2f  6143  nfrecs  6212  tfri3  6272  nffrec  6301  erovlem  6529  nfixpxy  6619  nfixp1  6620  xpf1o  6746  nneneq  6759  ac6sfi  6800  nfsup  6887  exmidomni  7022  fodjuomnilemdc  7024  ismkvnex  7037  mkvprop  7040  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  cc3  7100  caucvgsrlemgt1  7627  suplocsrlem  7640  axpre-suploclemres  7733  supinfneg  9417  infsupneg  9418  fimaxre2  11030  nfsum1  11157  nfsum  11158  fsumsplitf  11209  fsum2dlemstep  11235  fsum00  11263  nfcprod1  11355  nfcprod  11356  prodeq2  11358  zsupcllemstep  11674  bezoutlemmain  11722  bezoutlemzz  11726  bezout  11735  exmidunben  11975  ctiunctlemfo  11988  ctiunct  11989  mulcncf  12799  ellimc3apf  12837  limccnp2cntop  12854  bdsepnft  13256  bdsepnfALT  13258  bj-findis  13348  strcollnft  13353  strcollnfALT  13355  pw1nct  13371  isomninnlem  13400  trirec0  13412  iswomninnlem  13417  ismkvnnlem  13419