Theorem nfan 1901

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

Syntax hints:   ∧ wa 395  ⊤wtru 1543  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfnan  1902  nf3an  1903  hban  2307  nfeqf  2386  nfald2  2450  2ax6elem  2475  nfsb4t  2504  nfeu1  2590  eupicka  2635  mopick2  2638  2mo  2649  nfabd2  2923  2ralbida  3261  r19.12  3287  reean  3288  ralcom2  3349  cbvrmow  3377  nfrmow  3381  nfreuw  3382  cbvreu  3393  cbvrabw  3436  cbvrabwOLD  3437  nfrabw  3438  cbvrab  3441  ceqsex2  3495  vtocl2gafOLD  3537  vtocl3gaf  3538  spc2ed  3557  rspce  3567  eqvincf  3606  elrabf  3645  elrab3t  3647  rexab2  3659  morex  3679  reu2  3685  rmo3f  3694  reu2eqd  3696  sbc2iegf  3817  reu8nf  3829  rmo2  3839  rmo3  3841  csbiebt  3880  csbie2t  3889  cbvrabcsfw  3892  cbvreucsf  3895  cbvrabcsf  3896  nfdif  4083  nfin  4178  reusngf  4633  rexreusng  4638  reuprg0  4661  rabsnifsb  4681  nfop  4847  nfopd  4848  eluniab  4879  iuneqconst  4960  cbvopab  5172  cbvopab1  5174  cbvopab1g  5175  cbvopab2  5176  cbvopab1s  5177  mpteq12f  5185  nfmpt  5198  cbvmptf  5200  cbvmptfg  5201  axrep3  5230  axrep4OLD  5233  axrep5  5234  reusv2lem3  5347  axprlem4OLD  5376  axprlem5OLD  5377  nfpo  5546  nfso  5547  nffr  5605  nfwe  5607  nfxp  5665  opeliunxp  5699  opeliun2xp  5700  nfco  5822  elrnmpt1  5917  nfimad  6036  reuop  6259  iota2  6489  nffun  6523  imadif  6584  nffn  6599  nff  6666  nff1  6736  nffo  6753  nff1o  6780  nffvd  6854  fv3  6860  funimassd  6908  fvmptdf  6956  fompt  7072  f1ossf1o  7083  fmptco  7084  fsnex  7239  nfiso  7278  nfriotadw  7333  cbvriotaw  7334  nfriotad  7336  cbvriota  7338  riota2df  7348  riota5f  7353  oprabv  7428  nfoprab  7432  mpoeq123  7440  nfmpo  7450  cbvoprab1  7455  cbvoprab2  7456  cbvoprab12  7457  cbvoprab3  7459  cbvmpox  7461  ovmpodxf  7518  elovmporab  7614  elovmporab1w  7615  elovmporab1  7616  onminex  7757  fiun  7897  f1iun  7898  opabex3d  7919  opabex3rd  7920  opabex3  7921  dfoprab4f  8010  fmpox  8021  opeliunxp2f  8162  nffrecs  8235  frrlem4  8241  tfr3  8340  tz7.49  8386  naddsuc2  8639  erovlem  8762  nfixpw  8866  nfixp  8867  nfixp1  8868  xpf1o  9079  nneneq  9142  ac6sfi  9196  nfoi  9431  wdom2d  9497  infpssrlem4  10228  hsmexlem2  10349  hsmexlem4  10351  domtriomlem  10364  axdc3lem2  10373  axdc4lem  10377  zorn2lem4  10421  zorn2lem5  10422  konigthlem  10491  axextnd  10514  axrepndlem2  10516  axrepnd  10517  axunnd  10519  axpowndlem2  10521  axpowndlem4  10523  axpownd  10524  axregndlem2  10526  axregnd  10527  axinfndlem1  10528  axinfnd  10529  zfcndrep  10537  zfcndinf  10541  dedekind  11308  dedekindle  11309  fsuppmapnn0fiublem  13925  fsuppmapnn0fiub  13926  fsuppmapnn0fiubex  13927  reuccatpfxs1  14682  nfsum1  15625  nfsum  15626  fsumclf  15673  fsumsplitf  15677  fsumsplit1  15680  fsum2dlem  15705  fsum00  15733  nfcprod1  15843  nfcprod  15844  fprod2dlem  15915  fprodsplitf  15923  fprodsplit1f  15925  fprodle  15931  lcmfunsnlem1  16576  lcmfunsnlem2lem1  16577  lcmfunsnlem2  16579  mreexexd  17583  acsmapd  18489  gsum2d2lem  19914  dprd2d2  19987  gsummoncoe1  22264  gsummatr01lem4  22614  cpmatmcllem  22674  cayleyhamilton1  22848  neiptopnei  23088  neiptopreu  23089  neitr  23136  iunconnlem  23383  iunconn  23384  ptcnplem  23577  ptcnp  23578  xkocnv  23770  isfildlem  23813  utopsnneiplem  24203  isucn2  24234  cfilucfil  24515  restmetu  24526  ovolfiniun  25470  ovoliunlem3  25473  ovoliunnul  25476  volfiniun  25516  itg2splitlem  25717  itg2split  25718  isibl2  25735  nfitg  25744  cbvitg  25745  limciun  25863  2sqmo  27416  2sqreulem4  27433  bdaypw2n0bndlem  28471  istrkg2ld  28544  chirred  32482  sbc2iedf  32550  rspc2daf  32551  opreu2reuALT  32562  mo5f  32574  foresf1o  32590  iinabrex  32655  cbvdisjf  32657  disjabrex  32668  disjabrexf  32669  funimass4f  32726  2ndresdju  32738  fmptcof2  32746  fcomptf  32747  acunirnmpt2  32749  acunirnmpt2f  32750  aciunf1lem  32751  funcnv4mpt  32757  fnpreimac  32759  f1od2  32808  fpwrelmap  32822  xrofsup  32857  nn0min  32911  fprodex01  32916  fsumiunle  32920  prodindf  32954  suppgsumssiun  33165  isarchiofld  33292  elrgspnsubrunlem2  33341  nsgqusf1olem1  33505  nsgqusf1olem3  33507  elrspunidl  33520  deg1prod  33675  mplvrpmga  33721  esplyfval1  33749  vieta  33756  fedgmullem2  33807  irngnzply1  33868  reff  34016  locfinreflem  34017  cmpcref  34027  zarclsiin  34048  zarcmplem  34058  ordtconnlem1  34101  esumcl  34207  gsumesum  34236  esumlub  34237  esumcst  34240  esumrnmpt2  34245  esumfzf  34246  esumfsup  34247  hasheuni  34262  esumcvg  34263  esumgect  34267  esumcvgre  34268  esum2dlem  34269  esum2d  34270  esumiun  34271  ldsysgenld  34337  sigapildsyslem  34338  sigapildsys  34339  ldgenpisyslem1  34340  measvunilem  34389  measvunilem0  34390  measvuni  34391  measinblem  34397  voliune  34406  volfiniune  34407  volmeas  34408  oms0  34474  omssubadd  34477  eulerpartlemgvv  34553  dstrvprob  34649  breprexplema  34807  bnj919  34943  bnj1146  34966  bnj1379  35005  bnj849  35100  bnj916  35108  bnj964  35118  bnj1014  35136  bnj1123  35161  bnj1228  35186  bnj1307  35198  bnj1321  35202  bnj1398  35209  bnj1408  35211  bnj1444  35218  bnj1445  35219  bnj1446  35220  bnj1449  35223  bnj1467  35229  bnj1463  35230  bnj1489  35231  bnj1491  35232  bnj1312  35233  bnj1525  35244  dvelimalcased  35250  dvelimexcased  35252  fineqvrep  35289  cvmcov  35476  iota5f  35937  axextdist  36010  axextbdist  36011  nfwlim  36033  finminlem  36531  bj-dvelimdv  37090  bj-axreprepsep  37314  bj-opabco  37432  isbasisrelowllem1  37599  isbasisrelowllem2  37600  fvineqsneu  37655  fvineqsneq  37656  wl-cbvalnaed  37776  wl-2sb6d  37802  wl-sbalnae  37806  wl-mo2tf  37815  wl-eutf  37817  phpreu  37844  poimirlem26  37886  poimirlem27  37887  heicant  37895  mbfposadd  37907  ftc1anclem5  37937  indexdom  37974  filbcmb  37980  sdclem2  37982  sdclem1  37983  fdc1  37986  riotasv2d  39322  riotasv2s  39323  nfded2  39333  glbconxN  39743  pmapglb2xN  40137  cdlemefs32sn1aw  40779  mzpsubmpt  43089  mzpexpmpt  43091  eq0rabdioph  43122  eqrabdioph  43123  setindtr  43370  unielss  43564  nadd1suc  43738  ss2iundf  44004  scottabf  44585  mnuprdlem4  44620  ismnushort  44646  binomcxplemnotnn0  44701  iunconnlem2  45279  nfrelp  45294  modelaxreplem3  45325  modelaxrep  45326  permaxrep  45351  elunif  45365  rspcegf  45372  fnchoice  45378  refsumcn  45379  rfcnnnub  45385  uzwo4  45402  fiiuncl  45414  cbvmpo2  45445  cbvmpo1  45446  iinssiin  45477  disjf1  45531  disjrnmpt2  45536  disjf1o  45539  disjinfi  45540  choicefi  45547  axccdom  45569  dmrelrnrel  45573  axccd  45576  rnmptbddlem  45591  rnmptbd2lem  45595  infnsuprnmpt  45597  rnmptbdlem  45602  rnmptssbi  45607  upbdrech  45656  ssfiunibd  45660  supxrgere  45681  supxrgelem  45685  supxrge  45686  xralrple2  45702  infxr  45714  infxrunb2  45715  xrralrecnnle  45730  xrralrecnnge  45737  supxrunb3  45746  supxrleubrnmpt  45753  infleinf2  45761  unb2ltle  45762  rexabslelem  45765  suprleubrnmpt  45769  uzub  45778  supminfrnmpt  45792  supxrleubrnmptf  45798  infxrgelbrnmpt  45801  infrpgernmpt  45812  monoordxr  45829  monoord2xr  45831  caucvgbf  45836  cvgcaule  45838  iccshift  45867  iooshift  45871  iooiinicc  45891  iooiinioc  45905  fsummulc1f  45920  fsumf1of  45923  fsumreclf  45925  fsumlessf  45926  fmul01  45929  fmuldfeqlem1  45931  fmuldfeq  45932  fmul01lt1lem1  45933  fmul01lt1lem2  45934  fprodexp  45943  mccl  45947  fprodcnlem  45948  fprodcn  45949  climmulf  45953  climexp  45954  climsuse  45957  climrecf  45958  climinff  45960  climaddf  45964  mullimc  45965  islptre  45968  climf  45971  mullimcf  45972  rexlim2d  45974  idlimc  45975  limcperiod  45977  limcrecl  45978  islpcn  45986  limsupre  45988  limcleqr  45991  addlimc  45995  limclner  45998  climsubmpt  46007  climreclf  46011  climf2  46013  climeldmeqmpt  46015  clim2f2  46017  climfveqmpt  46018  fnlimfvre  46021  allbutfifvre  46022  climleltrp  46023  fnlimf  46025  fnlimabslt  46026  climfveqf  46027  climfveqmpt3  46029  climeldmeqf  46030  climeqf  46035  climeldmeqmpt3  46036  limsuppnfd  46049  limsupub  46051  climinf2lem  46053  climinf2  46054  limsuppnf  46058  limsupubuz  46060  climinf2mpt  46061  climinfmpt  46062  climinf3  46063  limsupmnflem  46067  limsupequz  46070  limsupre2  46072  limsupmnfuzlem  46073  limsupequzmptf  46078  limsupre3  46080  limsupre3uzlem  46082  limsupreuzmpt  46086  climisp  46093  lmbr3  46094  climrescn  46095  climxrrelem  46096  climxrre  46097  limsupub2  46159  liminflbuz2  46162  xlimmnfvlem2  46180  xlimmnfv  46181  xlimpnfvlem2  46184  xlimpnfv  46185  xlimmnfmpt  46190  xlimpnfmpt  46191  climxlim2lem  46192  cncficcgt0  46235  cncfioobd  46244  fprodsubrecnncnvlem  46254  fprodaddrecnncnvlem  46256  dvmptmulf  46284  dvnmul  46290  dvmptfprodlem  46291  dvmptfprod  46292  dvnprodlem1  46293  dvnprodlem2  46294  iblsplitf  46317  itgperiod  46328  stoweidlem3  46350  stoweidlem26  46373  stoweidlem27  46374  stoweidlem29  46376  stoweidlem31  46378  stoweidlem34  46381  stoweidlem35  46382  stoweidlem36  46383  stoweidlem39  46386  stoweidlem42  46389  stoweidlem43  46390  stoweidlem44  46391  stoweidlem46  46393  stoweidlem48  46395  stoweidlem49  46396  stoweidlem51  46398  stoweidlem52  46399  stoweidlem53  46400  stoweidlem54  46401  stoweidlem55  46402  stoweidlem56  46403  stoweidlem57  46404  stoweidlem58  46405  stoweidlem59  46406  stoweidlem60  46407  stoweidlem61  46408  stoweidlem62  46409  stoweid  46410  wallispilem3  46414  stirlinglem13  46433  stirling  46436  fourierdlem16  46470  fourierdlem21  46475  fourierdlem22  46476  fourierdlem31  46485  fourierdlem39  46493  fourierdlem48  46501  fourierdlem51  46504  fourierdlem68  46521  fourierdlem71  46524  fourierdlem73  46526  fourierdlem80  46533  fourierdlem81  46534  fourierdlem86  46539  fourierdlem87  46540  fourierdlem93  46546  fourierdlem94  46547  fourierdlem103  46556  fourierdlem104  46557  fourierdlem112  46565  fourierdlem113  46566  elaa2  46581  etransclem32  46613  salexct  46681  sge0revalmpt  46725  sge0f1o  46729  sge0lefi  46745  sge0resplit  46753  sge0lempt  46757  sge0iunmptlemre  46762  sge0fodjrnlem  46763  sge0iunmpt  46765  sge0ltfirpmpt2  46773  sge0isum  46774  sge0xp  46776  sge0isummpt2  46779  sge0xadd  46782  sge0pnffsumgt  46789  sge0gtfsumgt  46790  sge0uzfsumgt  46791  sge0reuz  46794  sge0reuzb  46795  iundjiun  46807  meadjiun  46813  ismeannd  46814  voliunsge0lem  46819  meaiunincf  46830  meaiuninc3v  46831  meaiuninc3  46832  meaiininc  46834  caragenfiiuncl  46862  omeiunltfirp  46866  ovnsubaddlem2  46918  hoidmvval0  46934  hoidmvlelem1  46942  hoidmvlelem3  46944  hoidmvlelem5  46946  ovnlecvr2  46957  hspdifhsp  46963  hoiqssbllem2  46970  hoiqssbllem3  46971  hspmbllem2  46974  opnvonmbllem2  46980  hoimbl2  47012  vonhoire  47019  iinhoiicc  47021  iunhoiioolem  47022  iunhoiioo  47023  vonioo  47029  vonicc  47032  vonn0ioo2  47037  vonn0icc2  47039  salpreimagelt  47054  salpreimalegt  47056  pimincfltioc  47063  pimdecfgtioo  47064  pimincfltioo  47065  preimageiingt  47067  preimaleiinlt  47068  salpreimagtge  47072  salpreimaltle  47073  salpreimalelt  47076  salpreimagtlt  47077  incsmflem  47088  issmflelem  47091  issmfle  47092  smfconst  47096  issmfgtlem  47102  issmfgt  47103  smfaddlem2  47111  smfadd  47112  decsmflem  47113  decsmf  47114  issmfgelem  47116  issmfge  47117  smflimlem2  47119  smflim  47124  smfresal  47135  smfrec  47136  smfmullem4  47141  smfmul  47142  smfpimcc  47155  smflimmpt  47157  smfsuplem1  47158  smfsupmpt  47162  smfsupxr  47163  smfinflem  47164  smfinfmpt  47166  smflimsuplem5  47171  smflimsuplem7  47173  smflimsuplem8  47174  smflimsupmpt  47176  smfliminflem  47177  smfliminfmpt  47179  smfpimne2  47187  fsupdm  47189  smfsupdmmbllem  47191  finfdm  47193  smfinfdmmbllem  47195  or2expropbilem2  47382  or2expropbi  47383  cfsetsnfsetf  47407  2reu8i  47462  nfdfat  47476  iccelpart  47782  ichnfim  47813  ich2exprop  47820  ichreuopeq  47822  sprsymrelfo  47846  reupr  47871  reuopreuprim  47875  2zrngmmgm  48601  cbvmpox2  48685  ovmpordxf  48688  1arymaptfo  48992  2arymaptfo  49003  iinfssclem3  49404  iinfssc  49405  iinfsubc  49406  setrec1  50039  pgindnf  50064  aacllem  50149