Theorem nfan 1544

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

Syntax hints:   ∧ wa 103  Ⅎwnf 1436

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 1423  ax-gen 1425  ax-4 1487

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

This theorem is referenced by:  nf3an  1545  cbvex2  1894  nfsbxyt  1916  sbcomxyyz  1945  nfsb4t  1989  clelab  2265  nfel  2290  2ralbida  2456  r19.29an  2574  reean  2599  nfrabxy  2611  cbvrexf  2649  cbvreu  2652  cbvrab  2684  ceqsex2  2726  vtocl2gaf  2753  rspce  2784  eqvincf  2810  elrabf  2838  elrab3t  2839  rexab2  2850  morex  2868  reu2  2872  rmo3f  2881  sbc2iegf  2979  rmo2ilem  2998  rmo3  3000  csbiebt  3039  csbie2t  3048  cbvrexcsf  3063  cbvreucsf  3064  cbvrabcsf  3065  nfopd  3722  eluniab  3748  dfnfc2  3754  nfdisjv  3918  disjiun  3924  nfopab  3996  cbvopab  3999  cbvopab1  4001  cbvopab2  4002  cbvopab1s  4003  mpteq12f  4008  nfmpt  4020  cbvmptf  4022  cbvmpt  4023  repizf2  4086  nfpo  4223  nfso  4224  nfwe  4277  onintonm  4433  peano2  4509  nfxp  4566  opeliunxp  4594  nfco  4704  elrnmpt1  4790  nfimad  4890  iota2  5114  dffun4f  5139  nffun  5146  imadif  5203  funimaexglem  5206  nffn  5219  nff  5269  nff1  5326  nffo  5344  nff1o  5365  fun11iun  5388  nffvd  5433  fv3  5444  fmptco  5586  nfiso  5707  cbvriota  5740  riota2df  5750  riota5f  5754  nfoprab  5823  mpoeq123  5830  nfmpo  5840  cbvoprab1  5843  cbvoprab2  5844  cbvoprab12  5845  cbvoprab3  5847  cbvmpox  5849  ovmpodxf  5896  opabex3d  6019  opabex3  6020  dfoprab4f  6091  fmpox  6098  spc2ed  6130  cnvoprab  6131  f1od2  6132  opeliunxp2f  6135  nfrecs  6204  tfri3  6264  nffrec  6293  erovlem  6521  nfixpxy  6611  nfixp1  6612  xpf1o  6738  nneneq  6751  ac6sfi  6792  nfsup  6879  exmidomni  7014  fodjuomnilemdc  7016  ismkvnex  7029  mkvprop  7032  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  caucvgsrlemgt1  7603  suplocsrlem  7616  axpre-suploclemres  7709  supinfneg  9390  infsupneg  9391  fimaxre2  10998  nfsum1  11125  nfsum  11126  fsumsplitf  11177  fsum2dlemstep  11203  fsum00  11231  nfcprod1  11323  nfcprod  11324  prodeq2  11326  zsupcllemstep  11638  bezoutlemmain  11686  bezoutlemzz  11690  bezout  11699  exmidunben  11939  ctiunctlemfo  11952  ctiunct  11953  mulcncf  12760  ellimc3apf  12798  limccnp2cntop  12815  bdsepnft  13085  bdsepnfALT  13087  bj-findis  13177  strcollnft  13182  isomninnlem  13225