Theorem nfan 1558

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

Syntax hints:   ∧ wa 103  Ⅎwnf 1453

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 1440  ax-gen 1442  ax-4 1503

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

This theorem is referenced by:  nf3an  1559  cbvex2  1915  nfsbxyt  1936  nfsbv  1940  sbcomxyyz  1965  nfsb4t  2007  clelab  2296  nfel  2321  2ralbida  2491  r19.29an  2612  reean  2638  nfrabxy  2650  cbvrexfw  2688  cbvrexf  2690  cbvreu  2694  cbvrab  2728  ceqsex2  2770  vtocl2gaf  2797  rspce  2829  eqvincf  2855  elrabf  2884  elrab3t  2885  rexab2  2896  morex  2914  reu2  2918  rmo3f  2927  sbc2iegf  3025  rmo2ilem  3044  rmo3  3046  csbiebt  3088  csbie2t  3097  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  nfopd  3780  eluniab  3806  dfnfc2  3812  nfdisjv  3976  disjiun  3982  nfopab  4055  cbvopab  4058  cbvopab1  4060  cbvopab2  4061  cbvopab1s  4062  mpteq12f  4067  nfmpt  4079  cbvmptf  4081  cbvmpt  4082  repizf2  4146  nfpo  4284  nfso  4285  nfwe  4338  onintonm  4499  peano2  4577  nfxp  4636  opeliunxp  4664  nfco  4774  elrnmpt1  4860  nfimad  4960  iota2  5186  dffun4f  5212  nffun  5219  imadif  5276  funimaexglem  5279  nffn  5292  nff  5342  nff1  5399  nffo  5417  nff1o  5438  fun11iun  5461  nffvd  5506  fv3  5517  fmptco  5659  nfiso  5782  cbvriota  5816  riota2df  5826  riota5f  5830  nfoprab  5902  mpoeq123  5909  nfmpo  5919  cbvoprab1  5922  cbvoprab2  5923  cbvoprab12  5924  cbvoprab3  5926  cbvmpox  5928  ovmpodxf  5975  opabex3d  6097  opabex3  6098  dfoprab4f  6169  fmpox  6176  spc2ed  6209  cnvoprab  6210  f1od2  6211  opeliunxp2f  6214  nfrecs  6283  tfri3  6343  nffrec  6372  erovlem  6601  nfixpxy  6691  nfixp1  6692  xpf1o  6818  nneneq  6831  ac6sfi  6872  nfsup  6965  exmidomni  7114  fodjuomnilemdc  7116  ismkvnex  7127  mkvprop  7130  exmidfodomrlemr  7166  exmidfodomrlemrALT  7167  cc3  7217  caucvgsrlemgt1  7744  suplocsrlem  7757  axpre-suploclemres  7850  supinfneg  9541  infsupneg  9542  fimaxre2  11177  nfsum1  11306  nfsum  11307  fsumsplitf  11358  fsum2dlemstep  11384  fsum00  11412  nfcprod1  11504  nfcprod  11505  prodeq2  11507  fprod2dlemstep  11572  fprodsplitf  11582  fprodsplit1f  11584  fprodap0f  11586  fprodle  11590  zsupcllemstep  11887  bezoutlemmain  11940  bezoutlemzz  11944  bezout  11953  exmidunben  12368  ctiunctlemfo  12381  ctiunct  12382  mulcncf  13344  ellimc3apf  13382  limccnp2cntop  13399  bdsepnft  13882  bdsepnfALT  13884  bj-findis  13974  strcollnft  13979  strcollnfALT  13981  pw1nct  13996  isomninnlem  14022  trirec0  14036  iswomninnlem  14041  ismkvnnlem  14044