Theorem nfan 1589

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

Syntax hints:   ∧ wa 104  Ⅎwnf 1484

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 1471  ax-gen 1473  ax-4 1534

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

This theorem is referenced by:  nf3an  1590  cbvex2  1947  nfsbxyt  1972  nfsbv  1976  sbcomxyyz  2001  nfsb4t  2043  clelab  2332  nfel  2358  2ralbida  2528  r19.29an  2649  reean  2676  nfrabw  2688  cbvrexfw  2730  cbvrexf  2732  cbvreu  2737  cbvrab  2771  ceqsex2  2814  vtocl2gaf  2841  rspce  2873  eqvincf  2899  elrabf  2928  elrab3t  2929  rexab2  2940  morex  2958  reu2  2962  rmo3f  2971  sbc2iegf  3070  rmo2ilem  3089  rmo3  3091  csbiebt  3134  csbie2t  3143  cbvrexcsf  3158  cbvreucsf  3159  cbvrabcsf  3160  nfopd  3838  eluniab  3864  dfnfc2  3870  nfdisjv  4035  disjiun  4042  nfopab  4116  cbvopab  4119  cbvopab1  4121  cbvopab2  4122  cbvopab1s  4123  mpteq12f  4128  nfmpt  4140  cbvmptf  4142  cbvmpt  4143  repizf2  4210  nfpo  4352  nfso  4353  nfwe  4406  onintonm  4569  peano2  4647  nfxp  4706  opeliunxp  4734  nfco  4847  elrnmpt1  4934  nfimad  5036  iota2  5266  dffun4f  5292  nffun  5299  imadif  5359  funimaexglem  5362  nffn  5375  nff  5428  nff1  5486  nffo  5504  nff1o  5527  fun11iun  5550  nffvd  5595  fv3  5606  fmptco  5753  nfiso  5882  cbvriota  5917  riota2df  5927  riota5f  5931  nfoprab  6004  mpoeq123  6011  nfmpo  6021  cbvoprab1  6024  cbvoprab2  6025  cbvoprab12  6026  cbvoprab3  6028  cbvmpox  6030  ovmpodxf  6078  elovmporab  6153  elovmporab1w  6154  opabex3d  6213  opabex3  6214  uchoice  6230  dfoprab4f  6286  fmpox  6293  spc2ed  6326  cnvoprab  6327  f1od2  6328  opeliunxp2f  6331  nfrecs  6400  tfri3  6460  nffrec  6489  erovlem  6721  nfixpxy  6811  nfixp1  6812  xpf1o  6948  nneneq  6961  ac6sfi  7002  opabfi  7042  nfsup  7101  exmidomni  7251  fodjuomnilemdc  7253  ismkvnex  7264  mkvprop  7267  exmidfodomrlemr  7317  exmidfodomrlemrALT  7318  cc3  7387  caucvgsrlemgt1  7915  suplocsrlem  7928  axpre-suploclemres  8021  supinfneg  9723  infsupneg  9724  zsupcllemstep  10379  nninfinf  10595  fimaxre2  11582  nfsum1  11711  nfsum  11712  fsumsplitf  11763  fsum2dlemstep  11789  fsum00  11817  nfcprod1  11909  nfcprod  11910  prodeq2  11912  fprod2dlemstep  11977  fprodsplitf  11987  fprodsplit1f  11989  fprodap0f  11991  fprodle  11995  bezoutlemmain  12363  bezoutlemzz  12367  bezout  12376  exmidunben  12841  ctiunctlemfo  12854  ctiunct  12855  mulcncf  15124  ellimc3apf  15176  limccnp2cntop  15193  bdsepnft  15897  bdsepnfALT  15899  bj-findis  15989  strcollnft  15994  strcollnfALT  15996  pw1nct  16014  isomninnlem  16043  trirec0  16057  iswomninnlem  16062  ismkvnnlem  16065