Theorem nfan 1509

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

Syntax hints:   ∧ wa 103  Ⅎwnf 1401

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-4 1452

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

This theorem is referenced by:  nf3an  1510  cbvex2  1852  nfsbxyt  1874  sbcomxyyz  1901  nfsb4t  1945  clelab  2219  nfel  2244  2ralbida  2410  r19.29an  2524  reean  2549  nfrabxy  2561  cbvrexf  2599  cbvreu  2602  cbvrab  2631  ceqsex2  2673  vtocl2gaf  2700  rspce  2731  eqvincf  2756  elrabf  2783  elrab3t  2784  rexab2  2795  morex  2813  reu2  2817  rmo3f  2826  sbc2iegf  2923  rmo2ilem  2942  rmo3  2944  csbiebt  2981  csbie2t  2990  cbvrexcsf  3005  cbvreucsf  3006  cbvrabcsf  3007  nfopd  3661  eluniab  3687  dfnfc2  3693  nfdisjv  3856  disjiun  3862  nfopab  3928  cbvopab  3931  cbvopab1  3933  cbvopab2  3934  cbvopab1s  3935  mpteq12f  3940  nfmpt  3952  cbvmptf  3954  cbvmpt  3955  repizf2  4018  nfpo  4152  nfso  4153  nfwe  4206  onintonm  4362  peano2  4438  nfxp  4494  opeliunxp  4522  nfco  4632  elrnmpt1  4718  nfimad  4816  iota2  5040  dffun4f  5065  nffun  5072  imadif  5128  funimaexglem  5131  nffn  5144  nff  5192  nff1  5249  nffo  5267  nff1o  5286  fun11iun  5309  nffvd  5352  fv3  5363  fmptco  5503  nfiso  5623  cbvriota  5656  riota2df  5666  riota5f  5670  nfoprab  5739  mpt2eq123  5746  nfmpt2  5755  cbvoprab1  5758  cbvoprab2  5759  cbvoprab12  5760  cbvoprab3  5762  cbvmpt2x  5764  ovmpt2dxf  5808  opabex3d  5930  opabex3  5931  dfoprab4f  6001  fmpt2x  6008  spc2ed  6036  cnvoprab  6037  f1od2  6038  opeliunxp2f  6041  nfrecs  6110  tfri3  6170  nffrec  6199  erovlem  6424  nfixpxy  6514  nfixp1  6515  xpf1o  6640  nneneq  6653  ac6sfi  6694  nfsup  6767  exmidomni  6885  fodjuomnilemdc  6887  mkvprop  6901  exmidfodomrlemr  6925  exmidfodomrlemrALT  6926  caucvgsrlemgt1  7437  supinfneg  9182  infsupneg  9183  fimaxre2  10789  nfsum1  10915  nfsum  10916  fsumsplitf  10967  fsum2dlemstep  10993  fsum00  11021  zsupcllemstep  11384  bezoutlemmain  11430  bezoutlemzz  11434  bezout  11443  mulcncf  12370  bdsepnft  12502  bdsepnfALT  12504  bj-findis  12598  strcollnft  12603