Theorem nfan 1934

Description: If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑 ∧ 𝜓). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) (Proof shortened by Wolf Lammen, 9-Oct-2021.)

Hypotheses

Ref	Expression
nfan.1	⊢ Ⅎ𝑥𝜑
nfan.2	⊢ Ⅎ𝑥𝜓

Assertion

Ref	Expression
nfan	⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Proof of Theorem nfan

Step	Hyp	Ref	Expression
1		nfan.1	. . . 4 ⊢ Ⅎ𝑥𝜑
2	1	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
3		nfan.2	. . . 4 ⊢ Ⅎ𝑥𝜓
4	3	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜓)
5	2, 4	nfand 1932	. 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ∧ 𝜓))
6	5	mptru 1577	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

This proof depends on syntax axioms:   ∧ wa 401  ⊤wtru 1571  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817

This theorem is used by:  nfnan  1935  nf3an  1936  hbanOLD  2337  nfeqf  2413  nfald2  2477  2ax6elem  2502  nfsb4t  2531  nfeu1  2617  eupicka  2662  mopick2  2665  2mo  2676  nfabd2  2949  2ralbida  3289  r19.12  3315  reean  3316  ralcom2  3366  cbvrmow  3394  nfrmow  3398  nfreuw  3399  cbvreu  3408  cbvrabw  3450  nfrabw  3451  cbvrab  3453  ceqsex2  3504  vtocl3gaf  3543  spc2ed  3559  rspce  3569  eqvincf  3607  elrabf  3645  elrab3t  3647  rexab2  3660  morex  3680  reu2  3686  rmo3f  3695  reu2eqd  3697  sbc2iegf  3817  reu8nf  3828  rmo2  3838  rmo3  3840  csbiebt  3880  csbie2t  3889  cbvrabcsfw  3892  cbvreucsf  3895  cbvrabcsf  3896  nfdif  4069  nfin  4124  reusngf  4635  rexreusng  4640  reuprg0  4663  rabsnifsb  4683  nfop  4852  nfopd  4853  eluniab  4884  iuneqconst  4966  cbvopab  5180  cbvopab1  5182  cbvopab1g  5183  cbvopab2  5184  cbvopab1s  5185  mpteq12f  5193  nfmpt  5206  cbvmptf  5208  cbvmptfg  5209  axrep3  5239  axrep5  5242  reusv2lem3  5366  nfpo  5569  nfso  5570  nffr  5628  nfwe  5630  nfxp  5688  opeliunxp  5722  opeliun2xp  5723  nfco  5849  elrnmpt1  5949  nfimad  6077  reuop  6314  iota2  6546  nffun  6582  imadif  6646  nffn  6660  nff  6727  nff1  6798  nffo  6817  nff1o  6844  nffvd  6920  fv3  6926  funimassd  6974  fvmptdf  7023  fompt  7142  f1ossf1o  7153  fmptco  7154  fsnex  7314  nfiso  7353  nfriotadw  7408  cbvriotaw  7409  nfriotad  7411  cbvriota  7413  riota2df  7423  riota5f  7428  oprabv  7503  nfoprab  7507  mpoeq123  7515  nfmpo  7525  cbvoprab1  7530  cbvoprab2  7531  cbvoprab12  7532  cbvoprab3  7534  cbvmpox  7536  ovmpodxf  7594  elovmporab  7691  elovmporab1w  7692  elovmporab1  7693  onminex  7840  fiun  7979  f1iun  7980  opabex3d  8001  opabex3rd  8002  opabex3  8003  dfoprab4f  8092  fmpox  8103  f1od2  8135  opeliunxp2f  8255  nffrecs  8329  frrlem4  8335  tfr3  8435  tz7.49  8483  naddsuc2  8739  erovlem  8862  nfixpw  8972  nfixp  8973  nfixp1  8974  xpf1o  9186  nneneq  9249  ac6sfi  9303  nfoi  9535  wdom2d  9601  scottabf  9966  setrec1  9999  infpssrlem4  10411  hsmexlem2  10532  hsmexlem4  10534  domtriomlem  10547  axdc3lem2  10556  axdc4lem  10560  zorn2lem4  10604  zorn2lem5  10605  konigthlem  10680  axextnd  10703  axrepndlem2  10705  axrepnd  10706  axunnd  10708  axpowndlem2  10710  axpowndlem4  10712  axpownd  10713  axregndlem2  10715  axregnd  10716  axinfndlem1  10717  axinfnd  10718  zfcndrep  10726  zfcndinf  10730  dedekind  11500  dedekindle  11501  fsuppmapnn0fiublem  14160  fsuppmapnn0fiub  14161  fsuppmapnn0fiubex  14162  reuccatpfxs1  14924  nfsum1  15886  nfsum  15887  fsumclf  15933  fsumsplitf  15937  fsumsplit1  15940  fsum2dlem  15965  fsum00  15994  nfcprod1  16106  nfcprod  16107  fprod2dlem  16176  fprodsplitf  16184  fprodsplit1f  16186  fprodle  16192  lcmfunsnlem1  16841  lcmfunsnlem2lem1  16842  lcmfunsnlem2  16844  mreexexd  17851  acsmapd  18757  gsum2d2lem  20217  dprd2d2  20290  gsummoncoe1  22656  gsummatr01lem4  23003  cpmatmcllem  23066  cayleyhamilton1  23240  neiptopnei  23480  neiptopreu  23481  neitr  23528  iunconnlem  23775  iunconn  23776  ptcnplem  23970  ptcnp  23971  xkocnv  24163  isfildlem  24206  utopsnneiplem  24596  isucn2  24627  cfilucfil  24908  restmetu  24919  ovolfiniun  25852  ovoliunlem3  25855  ovoliunnul  25858  volfiniun  25898  itg2splitlem  26099  itg2split  26100  isibl2  26117  nfitg  26125  cbvitg  26126  limciun  26244  2sqmo  27794  2sqreulem4  27811  bdaypw2n0bndlem  28879  istrkg2ld  28952  chirred  33027  sbc2iedf  33134  rspc2daf  33135  opreu2reuALT  33145  mo5f  33157  foresf1o  33172  iinabrex  33235  cbvdisjf  33237  disjabrex  33248  disjabrexf  33249  funimass4f  33303  2ndresdju  33315  fmptcof2  33323  fcomptf  33324  acunirnmpt2  33326  acunirnmpt2f  33327  aciunf1lem  33328  funcnv4mpt  33334  fnpreimac  33336  fpwrelmap  33395  xrofsup  33429  nn0min  33482  fprodex01  33486  fsumiunle  33490  prodindf  33499  suppgsumssiun  33703  isarchiofld  33830  elrgspnsubrunlem2  33879  nsgqusf1olem1  34034  nsgqusf1olem3  34036  elrspunidl  34048  deg1prod  34185  mplvrpmga  34247  esplyfval1  34275  vieta  34282  fedgmullem2  34332  irngnzply1  34393  reff  34541  locfinreflem  34542  cmpcref  34552  zarclsiin  34573  zarcmplem  34583  ordtconnlem1  34626  esumcl  34732  gsumesum  34761  esumlub  34762  esumcst  34765  esumrnmpt2  34770  esumfzf  34771  esumfsup  34772  hasheuni  34787  esumcvg  34788  esumgect  34792  esumcvgre  34793  esum2dlem  34794  esum2d  34795  esumiun  34796  ldsysgenld  34863  sigapildsyslem  34864  sigapildsys  34865  ldgenpisyslem1  34866  measvunilem  34915  measvunilem0  34916  measvuni  34917  measinblem  34923  voliune  34932  volfiniune  34933  volmeas  34934  oms0  34999  omssubadd  35002  eulerpartlemgvv  35078  dstrvprob  35174  breprexplema  35329  bnj919  35468  bnj1146  35491  bnj1379  35530  bnj849  35625  bnj916  35633  bnj964  35643  bnj1014  35661  bnj1123  35686  bnj1228  35711  bnj1307  35723  bnj1321  35727  bnj1398  35734  bnj1408  35736  bnj1444  35743  bnj1445  35744  bnj1446  35745  bnj1449  35748  bnj1467  35754  bnj1463  35755  bnj1489  35756  bnj1491  35757  bnj1312  35758  bnj1525  35769  dvelimalcased  35775  dvelimexcased  35777  reu6f  35779  fineqvrep  35882  srepdflem1  36085  srepdf  36087  cvmcov  36195  iota5f  36667  axextdist  36739  axextbdist  36740  nfwlim  36762  finminlem  37284  axtcond  37444  mh-inf3f1  37507  bj-dvelimdv  37941  bj-axreprepsep  38182  bj-opabco  38301  isbasisrelowllem1  38470  isbasisrelowllem2  38471  fvineqsneu  38526  fvineqsneq  38527  wl-cbvalnaed  38656  wl-2sb6d  38682  wl-sbalnae  38686  wl-mo2tf  38695  wl-eutf  38697  phpreu  38719  poimirlem26  38756  poimirlem27  38757  heicant  38765  mbfposadd  38777  ftc1anclem5  38807  indexdom  38860  filbcmb  38866  sdclem2  38868  sdclem1  38869  fdc1  38872  riotasv2d  40206  riotasv2s  40207  nfded2  40217  glbconxN  40627  pmapglb2xN  41021  cdlemefs32sn1aw  41663  mzpsubmpt  43947  mzpexpmpt  43949  eq0rabdioph  43980  eqrabdioph  43981  setindtr  44224  unielss  44412  nadd1suc  44586  ss2iundf  44851  mnuprdlem4  45451  ismnushort  45477  binomcxplemnotnn0  45532  iunconnlem2  46108  nfrelp  46134  modelaxreplem3  46165  modelaxrep  46166  permaxrep  46191  elunif  46238  rspcegf  46245  fnchoice  46251  refsumcn  46252  rfcnnnub  46258  uzwo4  46275  fiiuncl  46287  cbvmpo2  46317  cbvmpo1  46318  iinssiin  46349  disjf1  46403  disjrnmpt2  46408  disjf1o  46411  disjinfi  46412  choicefi  46419  axccdom  46440  dmrelrnrel  46444  axccd  46446  rnmptbddlem  46461  rnmptbd2lem  46465  infnsuprnmpt  46467  rnmptbdlem  46472  rnmptssbi  46477  upbdrech  46526  ssfiunibd  46530  supxrgere  46550  supxrgelem  46554  supxrge  46555  xralrple2  46571  infxr  46583  infxrunb2  46584  xrralrecnnle  46599  xrralrecnnge  46606  supxrunb3  46615  supxrleubrnmpt  46621  infleinf2  46629  unb2ltle  46630  rexabslelem  46633  suprleubrnmpt  46637  uzub  46646  supminfrnmpt  46660  supxrleubrnmptf  46666  infxrgelbrnmpt  46669  infrpgernmpt  46680  monoordxr  46697  monoord2xr  46699  caucvgbf  46704  cvgcaule  46706  iccshift  46735  iooshift  46739  iooiinicc  46759  iooiinioc  46773  fsummulc1f  46788  fsumf1of  46791  fsumreclf  46793  fsumlessf  46794  fmul01  46797  fmuldfeqlem1  46799  fmuldfeq  46800  fmul01lt1lem1  46801  fmul01lt1lem2  46802  fprodexp  46811  mccl  46815  fprodcnlem  46816  fprodcn  46817  climmulf  46821  climexp  46822  climsuse  46825  climrecf  46826  climinff  46828  climaddf  46832  mullimc  46833  islptre  46836  climf  46839  mullimcf  46840  rexlim2d  46842  idlimc  46843  limcperiod  46845  limcrecl  46846  islpcn  46854  limsupre  46856  limcleqr  46859  addlimc  46863  limclner  46866  climsubmpt  46875  climreclf  46879  climf2  46881  climeldmeqmpt  46883  clim2f2  46885  climfveqmpt  46886  fnlimfvre  46889  allbutfifvre  46890  climleltrp  46891  fnlimf  46893  fnlimabslt  46894  climfveqf  46895  climfveqmpt3  46897  climeldmeqf  46898  climeqf  46903  climeldmeqmpt3  46904  limsuppnfd  46917  limsupub  46919  climinf2lem  46921  climinf2  46922  limsuppnf  46926  limsupubuz  46928  climinf2mpt  46929  climinfmpt  46930  climinf3  46931  limsupmnflem  46935  limsupequz  46938  limsupre2  46940  limsupmnfuzlem  46941  limsupequzmptf  46946  limsupre3  46948  limsupre3uzlem  46950  limsupreuzmpt  46954  climisp  46961  lmbr3  46962  climrescn  46963  climxrrelem  46964  climxrre  46965  limsupub2  47027  liminflbuz2  47030  xlimmnfvlem2  47048  xlimmnfv  47049  xlimpnfvlem2  47052  xlimpnfv  47053  xlimmnfmpt  47058  xlimpnfmpt  47059  climxlim2lem  47060  cncficcgt0  47103  cncfioobd  47112  fprodsubrecnncnvlem  47122  fprodaddrecnncnvlem  47124  dvmptmulf  47152  dvnmul  47158  dvmptfprodlem  47159  dvmptfprod  47160  dvnprodlem1  47161  dvnprodlem2  47162  iblsplitf  47185  itgperiod  47196  stoweidlem3  47218  stoweidlem26  47241  stoweidlem27  47242  stoweidlem29  47244  stoweidlem31  47246  stoweidlem34  47249  stoweidlem35  47250  stoweidlem36  47251  stoweidlem39  47254  stoweidlem42  47257  stoweidlem43  47258  stoweidlem44  47259  stoweidlem46  47261  stoweidlem48  47263  stoweidlem49  47264  stoweidlem51  47266  stoweidlem52  47267  stoweidlem53  47268  stoweidlem54  47269  stoweidlem55  47270  stoweidlem56  47271  stoweidlem57  47272  stoweidlem58  47273  stoweidlem59  47274  stoweidlem60  47275  stoweidlem61  47276  stoweidlem62  47277  stoweid  47278  wallispilem3  47282  stirlinglem13  47301  stirling  47304  fourierdlem16  47338  fourierdlem21  47343  fourierdlem22  47344  fourierdlem31  47353  fourierdlem39  47361  fourierdlem48  47369  fourierdlem51  47372  fourierdlem68  47389  fourierdlem71  47392  fourierdlem73  47394  fourierdlem80  47401  fourierdlem81  47402  fourierdlem86  47407  fourierdlem87  47408  fourierdlem93  47414  fourierdlem94  47415  fourierdlem103  47424  fourierdlem104  47425  fourierdlem112  47433  fourierdlem113  47434  elaa2  47449  etransclem32  47481  salexct  47549  sge0revalmpt  47593  sge0f1o  47597  sge0lefi  47613  sge0resplit  47621  sge0lempt  47625  sge0iunmptlemre  47630  sge0fodjrnlem  47631  sge0iunmpt  47633  sge0ltfirpmpt2  47641  sge0isum  47642  sge0xp  47644  sge0isummpt2  47647  sge0xadd  47650  sge0pnffsumgt  47657  sge0gtfsumgt  47658  sge0uzfsumgt  47659  sge0reuz  47662  sge0reuzb  47663  iundjiun  47675  meadjiun  47681  ismeannd  47682  voliunsge0lem  47687  meaiunincf  47698  meaiuninc3v  47699  meaiuninc3  47700  meaiininc  47702  caragenfiiuncl  47730  omeiunltfirp  47734  ovnsubaddlem2  47786  hoidmvval0  47802  hoidmvlelem1  47810  hoidmvlelem3  47812  hoidmvlelem5  47814  ovnlecvr2  47825  hspdifhsp  47831  hoiqssbllem2  47838  hoiqssbllem3  47839  hspmbllem2  47842  opnvonmbllem2  47848  hoimbl2  47880  vonhoire  47887  iinhoiicc  47889  iunhoiioolem  47890  iunhoiioo  47891  vonioo  47897  vonicc  47900  vonn0ioo2  47905  vonn0icc2  47907  salpreimagelt  47922  salpreimalegt  47924  pimincfltioc  47931  pimdecfgtioo  47932  pimincfltioo  47933  preimageiingt  47935  preimaleiinlt  47936  salpreimagtge  47940  salpreimaltle  47941  salpreimalelt  47944  salpreimagtlt  47945  incsmflem  47956  issmflelem  47959  issmfle  47960  smfconst  47964  issmfgtlem  47970  issmfgt  47971  smfaddlem2  47979  smfadd  47980  decsmflem  47981  decsmf  47982  issmfgelem  47984  issmfge  47985  smflimlem2  47987  smflim  47992  smfresal  48003  smfrec  48004  smfmullem4  48009  smfmul  48010  smfpimcc  48023  smflimmpt  48025  smfsuplem1  48026  smfsupmpt  48030  smfsupxr  48031  smfinflem  48032  smfinfmpt  48034  smflimsuplem5  48039  smflimsuplem7  48041  smflimsuplem8  48042  smflimsupmpt  48044  smfliminflem  48045  smfliminfmpt  48047  smfpimne2  48055  fsupdm  48057  smfsupdmmbllem  48059  finfdm  48061  smfinfdmmbllem  48063  or2expropbilem2  48308  or2expropbi  48309  cfsetsnfsetf  48333  2reu8i  48389  nfdfat  48402  iccelpart  48720  ichnfim  48751  ich2exprop  48758  ichreuopeq  48760  sprsymrelfo  48784  reupr  48809  reuopreuprim  48813  2zrngmmgm  49554  cbvmpox2  49653  ovmpordxf  49656  1arymaptfo  49960  2arymaptfo  49971  iinfssclem3  50375  iinfssc  50376  iinfsubc  50377  pgindnf  51089  nfals  51179  nfrals  51180  nfalseu  51210  nfralseu  51211  aacllem  51219