Theorem nfan 1500

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

Syntax hints:   ∧ wa 102  Ⅎwnf 1392

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 1379  ax-gen 1381  ax-4 1443

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

This theorem is referenced by:  nf3an  1501  cbvex2  1842  nfsbxyt  1864  sbcomxyyz  1891  nfsb4t  1935  clelab  2209  nfel  2233  2ralbida  2395  r19.29an  2506  reean  2531  nfrabxy  2543  cbvrexf  2581  cbvreu  2584  cbvrab  2613  ceqsex2  2653  vtocl2gaf  2679  rspce  2710  eqvincf  2733  elrabf  2760  elrab3t  2761  rexab2  2772  morex  2790  reu2  2794  sbc2iegf  2898  rmo2ilem  2917  rmo3  2919  csbiebt  2956  csbie2t  2965  cbvrexcsf  2980  cbvreucsf  2981  cbvrabcsf  2982  nfopd  3622  eluniab  3648  dfnfc2  3654  nfdisjv  3813  nfopab  3881  cbvopab  3884  cbvopab1  3886  cbvopab2  3887  cbvopab1s  3888  mpteq12f  3893  nfmpt  3905  cbvmpt  3907  repizf2  3971  nfpo  4101  nfso  4102  nfwe  4155  onintonm  4306  peano2  4382  nfxp  4436  opeliunxp  4460  nfco  4568  elrnmpt1  4653  nfimad  4747  iota2  4969  dffun4f  4994  nffun  5000  imadif  5056  funimaexglem  5059  nffn  5072  nff  5120  nff1  5171  nffo  5189  nff1o  5208  fun11iun  5231  nffvd  5274  fv3  5285  fmptco  5421  nfiso  5540  cbvriota  5573  riota2df  5583  riota5f  5587  nfoprab  5652  mpt2eq123  5659  nfmpt2  5668  cbvoprab1  5671  cbvoprab2  5672  cbvoprab12  5673  cbvoprab3  5675  cbvmpt2x  5677  ovmpt2dxf  5721  opabex3d  5843  opabex3  5844  dfoprab4f  5914  fmpt2x  5921  spc2ed  5949  cnvoprab  5950  f1od2  5951  nfrecs  6020  tfri3  6080  nffrec  6109  erovlem  6330  xpf1o  6506  nneneq  6519  ac6sfi  6560  nfsup  6624  exmidomni  6735  fodjuomnilemdc  6736  exmidfodomrlemr  6765  exmidfodomrlemrALT  6766  caucvgsrlemgt1  7277  supinfneg  9008  infsupneg  9009  fimaxre2  10544  nfsum1  10628  nfsum  10629  zsupcllemstep  10808  bezoutlemmain  10854  bezoutlemzz  10858  bezout  10867  bdsepnft  11208  bdsepnfALT  11210  bj-findis  11304  strcollnft  11309