Theorem nfan 1899

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 1897	. 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ∧ 𝜓))
6	5	mptru 1547	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Syntax hints:   ∧ wa 395  ⊤wtru 1541  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfnan  1900  nf3an  1901  hban  2300  nfeqf  2379  nfald2  2443  2ax6elem  2468  nfsb4t  2497  nfeu1ALT  2582  eupicka  2627  mopick2  2630  2mo  2641  nfabd2  2915  2ralbida  3252  r19.12  3279  reean  3280  ralcom2  3342  cbvrmow  3372  nfrmow  3376  nfreuw  3377  cbvreu  3388  cbvrabw  3432  cbvrabwOLD  3433  nfrabw  3434  cbvrab  3437  ceqsex2  3492  vtocl2gafOLD  3537  vtocl3gaf  3538  spc2ed  3558  rspce  3568  eqvincf  3607  elrabf  3646  elrab3t  3649  rexab2  3661  morex  3681  reu2  3687  rmo3f  3696  reu2eqd  3698  sbc2iegf  3819  reu8nf  3831  rmo2  3841  rmo3  3843  csbiebt  3882  csbie2t  3891  cbvrabcsfw  3894  cbvreucsf  3897  cbvrabcsf  3898  nfdif  4082  nfin  4177  reusngf  4628  rexreusng  4633  reuprg0  4656  rabsnifsb  4676  nfop  4843  nfopd  4844  eluniab  4875  iuneqconst  4956  cbvopab  5167  cbvopab1  5169  cbvopab1g  5170  cbvopab2  5171  cbvopab1s  5172  mpteq12f  5180  nfmpt  5193  cbvmptf  5195  cbvmptfg  5196  axrep3  5225  axrep4OLD  5228  axrep5  5229  reusv2lem3  5342  axprlem4OLD  5371  axprlem5OLD  5372  nfpo  5537  nfso  5538  nffr  5596  nfwe  5598  nfxp  5656  opeliunxp  5690  opeliun2xp  5691  nfco  5812  elrnmpt1  5906  nfimad  6024  reuop  6245  iota2  6475  nffun  6509  imadif  6570  nffn  6585  nff  6652  nff1  6722  nffo  6739  nff1o  6766  nffvd  6838  fv3  6844  funimassd  6893  fvmptdf  6940  fompt  7056  f1ossf1o  7066  fmptco  7067  fsnex  7224  nfiso  7263  nfriotadw  7318  cbvriotaw  7319  nfriotad  7321  cbvriota  7323  riota2df  7333  riota5f  7338  oprabv  7413  nfoprab  7417  mpoeq123  7425  nfmpo  7435  cbvoprab1  7440  cbvoprab2  7441  cbvoprab12  7442  cbvoprab3  7444  cbvmpox  7446  ovmpodxf  7503  elovmporab  7599  elovmporab1w  7600  elovmporab1  7601  onminex  7742  fiun  7885  f1iun  7886  opabex3d  7907  opabex3rd  7908  opabex3  7909  dfoprab4f  7998  fmpox  8009  opeliunxp2f  8150  nffrecs  8223  frrlem4  8229  tfr3  8328  tz7.49  8374  naddsuc2  8626  erovlem  8747  nfixpw  8850  nfixp  8851  nfixp1  8852  xpf1o  9063  nneneq  9130  ac6sfi  9189  nfoi  9425  wdom2d  9491  infpssrlem4  10219  hsmexlem2  10340  hsmexlem4  10342  domtriomlem  10355  axdc3lem2  10364  axdc4lem  10368  zorn2lem4  10412  zorn2lem5  10413  konigthlem  10481  axextnd  10504  axrepndlem2  10506  axrepnd  10507  axunnd  10509  axpowndlem2  10511  axpowndlem4  10513  axpownd  10514  axregndlem2  10516  axregnd  10517  axinfndlem1  10518  axinfnd  10519  zfcndrep  10527  zfcndinf  10531  dedekind  11297  dedekindle  11298  fsuppmapnn0fiublem  13915  fsuppmapnn0fiub  13916  fsuppmapnn0fiubex  13917  reuccatpfxs1  14671  nfsum1  15615  nfsum  15616  fsumclf  15663  fsumsplitf  15667  fsumsplit1  15670  fsum2dlem  15695  fsum00  15723  nfcprod1  15833  nfcprod  15834  fprod2dlem  15905  fprodsplitf  15913  fprodsplit1f  15915  fprodle  15921  lcmfunsnlem1  16566  lcmfunsnlem2lem1  16567  lcmfunsnlem2  16569  mreexexd  17572  acsmapd  18478  gsum2d2lem  19870  dprd2d2  19943  gsummoncoe1  22211  gsummatr01lem4  22561  cpmatmcllem  22621  cayleyhamilton1  22795  neiptopnei  23035  neiptopreu  23036  neitr  23083  iunconnlem  23330  iunconn  23331  ptcnplem  23524  ptcnp  23525  xkocnv  23717  isfildlem  23760  utopsnneiplem  24151  isucn2  24182  cfilucfil  24463  restmetu  24474  ovolfiniun  25418  ovoliunlem3  25421  ovoliunnul  25424  volfiniun  25464  itg2splitlem  25665  itg2split  25666  isibl2  25683  nfitg  25692  cbvitg  25693  limciun  25811  2sqmo  27364  2sqreulem4  27381  istrkg2ld  28423  chirred  32357  sbc2iedf  32427  rspc2daf  32428  opreu2reuALT  32439  mo5f  32451  foresf1o  32466  iinabrex  32531  cbvdisjf  32533  disjabrex  32544  disjabrexf  32545  funimass4f  32594  2ndresdju  32606  fmptcof2  32614  fcomptf  32615  acunirnmpt2  32617  acunirnmpt2f  32618  aciunf1lem  32619  funcnv4mpt  32626  fnpreimac  32628  f1od2  32677  fpwrelmap  32689  xrofsup  32723  nn0min  32778  fprodex01  32783  fsumiunle  32787  prodindf  32819  isarchiofld  33151  elrgspnsubrunlem2  33198  nsgqusf1olem1  33360  nsgqusf1olem3  33362  elrspunidl  33375  fedgmullem2  33602  irngnzply1  33662  reff  33805  locfinreflem  33806  cmpcref  33816  zarclsiin  33837  zarcmplem  33847  ordtconnlem1  33890  esumcl  33996  gsumesum  34025  esumlub  34026  esumcst  34029  esumrnmpt2  34034  esumfzf  34035  esumfsup  34036  hasheuni  34051  esumcvg  34052  esumgect  34056  esumcvgre  34057  esum2dlem  34058  esum2d  34059  esumiun  34060  ldsysgenld  34126  sigapildsyslem  34127  sigapildsys  34128  ldgenpisyslem1  34129  measvunilem  34178  measvunilem0  34179  measvuni  34180  measinblem  34186  voliune  34195  volfiniune  34196  volmeas  34197  oms0  34264  omssubadd  34267  eulerpartlemgvv  34343  dstrvprob  34439  breprexplema  34597  bnj919  34733  bnj1146  34757  bnj1379  34796  bnj849  34891  bnj916  34899  bnj964  34909  bnj1014  34927  bnj1123  34952  bnj1228  34977  bnj1307  34989  bnj1321  34993  bnj1398  35000  bnj1408  35002  bnj1444  35009  bnj1445  35010  bnj1446  35011  bnj1449  35014  bnj1467  35020  bnj1463  35021  bnj1489  35022  bnj1491  35023  bnj1312  35024  bnj1525  35035  dvelimalcased  35041  dvelimexcased  35043  fineqvrep  35069  cvmcov  35235  iota5f  35696  axextdist  35772  axextbdist  35773  nfwlim  35795  finminlem  36291  bj-dvelimdv  36824  bj-opabco  37161  isbasisrelowllem1  37328  isbasisrelowllem2  37329  fvineqsneu  37384  fvineqsneq  37385  wl-cbvalnaed  37505  wl-2sb6d  37531  wl-sbalnae  37535  wl-mo2tf  37544  wl-eutf  37546  wl-ax11-lem3  37560  phpreu  37583  poimirlem26  37625  poimirlem27  37626  heicant  37634  mbfposadd  37646  ftc1anclem5  37676  indexdom  37713  filbcmb  37719  sdclem2  37721  sdclem1  37722  fdc1  37725  riotasv2d  38935  riotasv2s  38936  nfded2  38946  glbconxN  39357  pmapglb2xN  39751  cdlemefs32sn1aw  40393  mzpsubmpt  42716  mzpexpmpt  42718  eq0rabdioph  42749  eqrabdioph  42750  setindtr  42997  unielss  43191  nadd1suc  43365  ss2iundf  43632  scottabf  44213  mnuprdlem4  44248  ismnushort  44274  binomcxplemnotnn0  44329  iunconnlem2  44908  nfrelp  44923  modelaxreplem3  44954  modelaxrep  44955  permaxrep  44980  elunif  44994  rspcegf  45001  fnchoice  45007  refsumcn  45008  rfcnnnub  45014  uzwo4  45031  fiiuncl  45043  cbvmpo2  45075  cbvmpo1  45076  iinssiin  45107  disjf1  45161  disjrnmpt2  45166  disjf1o  45169  disjinfi  45170  choicefi  45178  axccdom  45200  dmrelrnrel  45204  axccd  45207  rnmptbddlem  45222  rnmptbd2lem  45226  infnsuprnmpt  45228  rnmptbdlem  45233  rnmptssbi  45238  upbdrech  45287  ssfiunibd  45291  supxrgere  45313  supxrgelem  45317  supxrge  45318  xralrple2  45334  infxr  45347  infxrunb2  45348  xrralrecnnle  45363  xrralrecnnge  45370  supxrunb3  45379  supxrleubrnmpt  45386  infleinf2  45394  unb2ltle  45395  rexabslelem  45398  suprleubrnmpt  45402  uzub  45411  supminfrnmpt  45425  supxrleubrnmptf  45431  infxrgelbrnmpt  45434  infrpgernmpt  45445  monoordxr  45462  monoord2xr  45464  caucvgbf  45469  cvgcaule  45471  iccshift  45500  iooshift  45504  iooiinicc  45524  iooiinioc  45538  fsummulc1f  45553  fsumf1of  45556  fsumreclf  45558  fsumlessf  45559  fmul01  45562  fmuldfeqlem1  45564  fmuldfeq  45565  fmul01lt1lem1  45566  fmul01lt1lem2  45567  fprodexp  45576  mccl  45580  fprodcnlem  45581  fprodcn  45582  climmulf  45586  climexp  45587  climsuse  45590  climrecf  45591  climinff  45593  climaddf  45597  mullimc  45598  islptre  45601  climf  45604  mullimcf  45605  rexlim2d  45607  idlimc  45608  limcperiod  45610  limcrecl  45611  islpcn  45621  limsupre  45623  limcleqr  45626  addlimc  45630  limclner  45633  climsubmpt  45642  climreclf  45646  climf2  45648  climeldmeqmpt  45650  clim2f2  45652  climfveqmpt  45653  fnlimfvre  45656  allbutfifvre  45657  climleltrp  45658  fnlimf  45660  fnlimabslt  45661  climfveqf  45662  climfveqmpt3  45664  climeldmeqf  45665  climeqf  45670  climeldmeqmpt3  45671  limsuppnfd  45684  limsupub  45686  climinf2lem  45688  climinf2  45689  limsuppnf  45693  limsupubuz  45695  climinf2mpt  45696  climinfmpt  45697  climinf3  45698  limsupmnflem  45702  limsupequz  45705  limsupre2  45707  limsupmnfuzlem  45708  limsupequzmptf  45713  limsupre3  45715  limsupre3uzlem  45717  limsupreuzmpt  45721  climisp  45728  lmbr3  45729  climrescn  45730  climxrrelem  45731  climxrre  45732  limsupub2  45794  liminflbuz2  45797  xlimmnfvlem2  45815  xlimmnfv  45816  xlimpnfvlem2  45819  xlimpnfv  45820  xlimmnfmpt  45825  xlimpnfmpt  45826  climxlim2lem  45827  cncficcgt0  45870  cncfioobd  45879  fprodsubrecnncnvlem  45889  fprodaddrecnncnvlem  45891  dvmptmulf  45919  dvnmul  45925  dvmptfprodlem  45926  dvmptfprod  45927  dvnprodlem1  45928  dvnprodlem2  45929  iblsplitf  45952  itgperiod  45963  stoweidlem3  45985  stoweidlem26  46008  stoweidlem27  46009  stoweidlem29  46011  stoweidlem31  46013  stoweidlem34  46016  stoweidlem35  46017  stoweidlem36  46018  stoweidlem39  46021  stoweidlem42  46024  stoweidlem43  46025  stoweidlem44  46026  stoweidlem46  46028  stoweidlem48  46030  stoweidlem49  46031  stoweidlem51  46033  stoweidlem52  46034  stoweidlem53  46035  stoweidlem54  46036  stoweidlem55  46037  stoweidlem56  46038  stoweidlem57  46039  stoweidlem58  46040  stoweidlem59  46041  stoweidlem60  46042  stoweidlem61  46043  stoweidlem62  46044  stoweid  46045  wallispilem3  46049  stirlinglem13  46068  stirling  46071  fourierdlem16  46105  fourierdlem21  46110  fourierdlem22  46111  fourierdlem31  46120  fourierdlem39  46128  fourierdlem48  46136  fourierdlem51  46139  fourierdlem68  46156  fourierdlem71  46159  fourierdlem73  46161  fourierdlem80  46168  fourierdlem81  46169  fourierdlem86  46174  fourierdlem87  46175  fourierdlem93  46181  fourierdlem94  46182  fourierdlem103  46191  fourierdlem104  46192  fourierdlem112  46200  fourierdlem113  46201  elaa2  46216  etransclem32  46248  salexct  46316  sge0revalmpt  46360  sge0f1o  46364  sge0lefi  46380  sge0resplit  46388  sge0lempt  46392  sge0iunmptlemre  46397  sge0fodjrnlem  46398  sge0iunmpt  46400  sge0ltfirpmpt2  46408  sge0isum  46409  sge0xp  46411  sge0isummpt2  46414  sge0xadd  46417  sge0pnffsumgt  46424  sge0gtfsumgt  46425  sge0uzfsumgt  46426  sge0reuz  46429  sge0reuzb  46430  iundjiun  46442  meadjiun  46448  ismeannd  46449  voliunsge0lem  46454  meaiunincf  46465  meaiuninc3v  46466  meaiuninc3  46467  meaiininc  46469  caragenfiiuncl  46497  omeiunltfirp  46501  ovnsubaddlem2  46553  hoidmvval0  46569  hoidmvlelem1  46577  hoidmvlelem3  46579  hoidmvlelem5  46581  ovnlecvr2  46592  hspdifhsp  46598  hoiqssbllem2  46605  hoiqssbllem3  46606  hspmbllem2  46609  opnvonmbllem2  46615  hoimbl2  46647  vonhoire  46654  iinhoiicc  46656  iunhoiioolem  46657  iunhoiioo  46658  vonioo  46664  vonicc  46667  vonn0ioo2  46672  vonn0icc2  46674  salpreimagelt  46689  salpreimalegt  46691  pimincfltioc  46698  pimdecfgtioo  46699  pimincfltioo  46700  preimageiingt  46702  preimaleiinlt  46703  salpreimagtge  46707  salpreimaltle  46708  salpreimalelt  46711  salpreimagtlt  46712  incsmflem  46723  issmflelem  46726  issmfle  46727  smfconst  46731  issmfgtlem  46737  issmfgt  46738  smfaddlem2  46746  smfadd  46747  decsmflem  46748  decsmf  46749  issmfgelem  46751  issmfge  46752  smflimlem2  46754  smflim  46759  smfresal  46770  smfrec  46771  smfmullem4  46776  smfmul  46777  smfpimcc  46790  smflimmpt  46792  smfsuplem1  46793  smfsupmpt  46797  smfsupxr  46798  smfinflem  46799  smfinfmpt  46801  smflimsuplem5  46806  smflimsuplem7  46808  smflimsuplem8  46809  smflimsupmpt  46811  smfliminflem  46812  smfliminfmpt  46814  smfpimne2  46822  fsupdm  46824  smfsupdmmbllem  46826  finfdm  46828  smfinfdmmbllem  46830  or2expropbilem2  47018  or2expropbi  47019  cfsetsnfsetf  47043  2reu8i  47098  nfdfat  47112  iccelpart  47418  ichnfim  47449  ich2exprop  47456  ichreuopeq  47458  sprsymrelfo  47482  reupr  47507  reuopreuprim  47511  2zrngmmgm  48224  cbvmpox2  48308  ovmpordxf  48311  1arymaptfo  48616  2arymaptfo  48627  iinfssclem3  49029  iinfssc  49030  iinfsubc  49031  setrec1  49664  pgindnf  49689  aacllem  49774