Theorem nfan 1614

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

Syntax hints:   ∧ wa 104  Ⅎwnf 1509

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 1496  ax-gen 1498  ax-4 1559

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

This theorem is referenced by:  nf3an  1615  cbvex2  1974  nfsbxyt  1999  nfsbv  2003  sbcomxyyz  2028  nfsb4t  2070  clelab  2362  nfel  2395  2ralbida  2565  r19.29an  2687  reean  2714  nfrabw  2727  cbvrmow  2729  cbvrexfw  2770  cbvrexf  2772  cbvreu  2778  cbvrab  2813  ceqsex2  2857  vtocl2gaf  2884  rspce  2918  eqvincf  2944  elrabf  2973  elrab3t  2974  rexab2  2985  morex  3003  reu2  3007  rmo3f  3016  sbc2iegf  3115  reu8nf  3126  rmo2ilem  3135  rmo3  3137  csbiebt  3180  csbie2t  3189  cbvrexcsf  3204  cbvreucsf  3205  cbvrabcsf  3206  rabsnifsb  3759  nfopd  3902  eluniab  3928  dfnfc2  3934  nfdisjv  4099  disjiun  4106  nfopab  4180  cbvopab  4183  cbvopab1  4185  cbvopab2  4186  cbvopab1s  4187  mpteq12f  4192  nfmpt  4204  cbvmptf  4206  cbvmpt  4207  repizf2  4277  nfpo  4424  nfso  4425  nfwe  4478  onintonm  4641  peano2  4719  nfxp  4778  opeliunxp  4807  nfco  4922  elrnmpt1  5010  nfimad  5112  iota2  5344  dffun4f  5370  nffun  5377  imadif  5438  funimaexglem  5441  nffn  5454  nff  5507  nff1  5573  nffo  5591  nff1o  5614  fun11iun  5637  nffvd  5684  fv3  5695  fmptco  5845  nfiso  5981  cbvriota  6017  riota2df  6027  riota5f  6032  nfoprab  6107  mpoeq123  6114  nfmpo  6124  cbvoprab1  6127  cbvoprab2  6128  cbvoprab12  6129  cbvoprab3  6131  cbvmpox  6133  ovmpodxf  6181  elovmporab  6256  elovmporab1w  6257  opabex3d  6316  opabex3  6317  uchoice  6333  dfoprab4f  6389  fmpox  6398  spc2ed  6431  cnvoprab  6432  f1od2  6433  opeliunxp2f  6471  nfrecs  6540  tfri3  6600  nffrec  6629  erovlem  6863  nfixpxy  6954  nfixp1  6955  modom  7063  xpf1o  7099  nneneq  7113  ac6sfi  7157  opabfi  7202  nfsup  7285  exmidomni  7435  fodjuomnilemdc  7437  ismkvnex  7448  mkvprop  7451  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  cc3  7587  caucvgsrlemgt1  8115  suplocsrlem  8128  axpre-suploclemres  8221  supinfneg  9933  infsupneg  9934  zsupcllemstep  10596  nninfinf  10812  reuccatpfxs1  11447  fimaxre2  11920  nfsum1  12049  nfsum  12050  fsumsplitf  12102  fsum2dlemstep  12128  fsum00  12156  nfcprod1  12248  nfcprod  12249  prodeq2  12251  fprod2dlemstep  12316  fprodsplitf  12326  fprodsplit1f  12328  fprodap0f  12330  fprodle  12334  bezoutlemmain  12702  bezoutlemzz  12706  bezout  12715  exmidunben  13198  ctiunctlemfo  13211  ctiunct  13212  mulcncf  15522  ellimc3apf  15574  limccnp2cntop  15591  bdsepnft  16706  bdsepnfALT  16708  bj-findis  16798  strcollnft  16803  strcollnfALT  16805  pw1nct  16826  isomninnlem  16863  trirec0  16877  iswomninnlem  16883  ismkvnnlem  16886