Theorem nfan 1931

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

This proof depends on syntax axioms:   ∧ wa 401  ⊤wtru 1570  Ⅎwnf 1815

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

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816

This theorem is used by:  nfnan  1932  nf3an  1933  hban  2333  nfeqf  2410  nfald2  2474  2ax6elem  2499  nfsb4t  2528  nfeu1  2614  eupicka  2659  mopick2  2662  2mo  2673  nfabd2  2945  2ralbida  3285  r19.12  3311  reean  3312  ralcom2  3362  cbvrmow  3390  nfrmow  3394  nfreuw  3395  cbvreu  3404  cbvrabw  3446  nfrabw  3447  cbvrab  3449  ceqsex2  3500  vtocl3gaf  3539  spc2ed  3555  rspce  3565  eqvincf  3603  elrabf  3641  elrab3t  3643  rexab2  3656  morex  3676  reu2  3682  rmo3f  3691  reu2eqd  3693  sbc2iegf  3812  reu8nf  3823  rmo2  3833  rmo3  3835  csbiebt  3875  csbie2t  3884  cbvrabcsfw  3887  cbvreucsf  3890  cbvrabcsf  3891  nfdif  4066  nfin  4121  reusngf  4634  rexreusng  4639  reuprg0  4662  rabsnifsb  4682  nfop  4848  nfopd  4849  eluniab  4880  iuneqconst  4962  cbvopab  5176  cbvopab1  5178  cbvopab1g  5179  cbvopab2  5180  cbvopab1s  5181  mpteq12f  5189  nfmpt  5202  cbvmptf  5204  cbvmptfg  5205  axrep3  5235  axrep5  5238  reusv2lem3  5361  nfpo  5564  nfso  5565  nffr  5623  nfwe  5625  nfxp  5683  opeliunxp  5717  opeliun2xp  5718  nfco  5842  elrnmpt1  5941  nfimad  6064  reuop  6296  iota2  6527  nffun  6562  imadif  6624  nffn  6638  nff  6705  nff1  6776  nffo  6795  nff1o  6822  nffvd  6897  fv3  6903  funimassd  6951  fvmptdf  7000  fompt  7118  f1ossf1o  7129  fmptco  7130  fsnex  7291  nfiso  7330  nfriotadw  7385  cbvriotaw  7386  nfriotad  7388  cbvriota  7390  riota2df  7400  riota5f  7405  oprabv  7480  nfoprab  7484  mpoeq123  7492  nfmpo  7502  cbvoprab1  7507  cbvoprab2  7508  cbvoprab12  7509  cbvoprab3  7511  cbvmpox  7513  ovmpodxf  7570  elovmporab  7667  elovmporab1w  7668  elovmporab1  7669  onminex  7816  fiun  7955  f1iun  7956  opabex3d  7977  opabex3rd  7978  opabex3  7979  dfoprab4f  8067  fmpox  8078  opeliunxp2f  8228  nffrecs  8302  frrlem4  8308  tfr3  8408  tz7.49  8456  naddsuc2  8712  erovlem  8835  nfixpw  8945  nfixp  8946  nfixp1  8947  xpf1o  9159  nneneq  9222  ac6sfi  9276  nfoi  9509  wdom2d  9575  scottabf  9940  setrec1  9973  infpssrlem4  10385  hsmexlem2  10506  hsmexlem4  10508  domtriomlem  10521  axdc3lem2  10530  axdc4lem  10534  zorn2lem4  10578  zorn2lem5  10579  konigthlem  10654  axextnd  10677  axrepndlem2  10679  axrepnd  10680  axunnd  10682  axpowndlem2  10684  axpowndlem4  10686  axpownd  10687  axregndlem2  10689  axregnd  10690  axinfndlem1  10691  axinfnd  10692  zfcndrep  10700  zfcndinf  10704  dedekind  11474  dedekindle  11475  fsuppmapnn0fiublem  14134  fsuppmapnn0fiub  14135  fsuppmapnn0fiubex  14136  reuccatpfxs1  14897  nfsum1  15858  nfsum  15859  fsumclf  15905  fsumsplitf  15909  fsumsplit1  15912  fsum2dlem  15937  fsum00  15966  nfcprod1  16078  nfcprod  16079  fprod2dlem  16148  fprodsplitf  16156  fprodsplit1f  16158  fprodle  16164  lcmfunsnlem1  16813  lcmfunsnlem2lem1  16814  lcmfunsnlem2  16816  mreexexd  17823  acsmapd  18729  gsum2d2lem  20188  dprd2d2  20261  gsummoncoe1  22627  gsummatr01lem4  22974  cpmatmcllem  23037  cayleyhamilton1  23211  neiptopnei  23451  neiptopreu  23452  neitr  23499  iunconnlem  23746  iunconn  23747  ptcnplem  23941  ptcnp  23942  xkocnv  24134  isfildlem  24177  utopsnneiplem  24567  isucn2  24598  cfilucfil  24879  restmetu  24890  ovolfiniun  25823  ovoliunlem3  25826  ovoliunnul  25829  volfiniun  25869  itg2splitlem  26070  itg2split  26071  isibl2  26088  nfitg  26096  cbvitg  26097  limciun  26215  2sqmo  27765  2sqreulem4  27782  bdaypw2n0bndlem  28850  istrkg2ld  28923  chirred  32998  sbc2iedf  33105  rspc2daf  33106  opreu2reuALT  33116  mo5f  33128  foresf1o  33143  iinabrex  33206  cbvdisjf  33208  disjabrex  33219  disjabrexf  33220  funimass4f  33274  2ndresdju  33286  fmptcof2  33294  fcomptf  33295  acunirnmpt2  33297  acunirnmpt2f  33298  aciunf1lem  33299  funcnv4mpt  33305  fnpreimac  33307  f1od2  33354  fpwrelmap  33368  xrofsup  33402  nn0min  33455  fprodex01  33459  fsumiunle  33463  prodindf  33472  suppgsumssiun  33676  isarchiofld  33803  elrgspnsubrunlem2  33852  nsgqusf1olem1  34007  nsgqusf1olem3  34009  elrspunidl  34021  deg1prod  34158  mplvrpmga  34220  esplyfval1  34248  vieta  34255  fedgmullem2  34305  irngnzply1  34366  reff  34514  locfinreflem  34515  cmpcref  34525  zarclsiin  34546  zarcmplem  34556  ordtconnlem1  34599  esumcl  34705  gsumesum  34734  esumlub  34735  esumcst  34738  esumrnmpt2  34743  esumfzf  34744  esumfsup  34745  hasheuni  34760  esumcvg  34761  esumgect  34765  esumcvgre  34766  esum2dlem  34767  esum2d  34768  esumiun  34769  ldsysgenld  34836  sigapildsyslem  34837  sigapildsys  34838  ldgenpisyslem1  34839  measvunilem  34888  measvunilem0  34889  measvuni  34890  measinblem  34896  voliune  34905  volfiniune  34906  volmeas  34907  oms0  34972  omssubadd  34975  eulerpartlemgvv  35051  dstrvprob  35147  breprexplema  35302  bnj919  35441  bnj1146  35464  bnj1379  35503  bnj849  35598  bnj916  35606  bnj964  35616  bnj1014  35634  bnj1123  35659  bnj1228  35684  bnj1307  35696  bnj1321  35700  bnj1398  35707  bnj1408  35709  bnj1444  35716  bnj1445  35717  bnj1446  35718  bnj1449  35721  bnj1467  35727  bnj1463  35728  bnj1489  35729  bnj1491  35730  bnj1312  35731  bnj1525  35742  dvelimalcased  35748  dvelimexcased  35750  fineqvrep  35831  cvmcov  36097  iota5f  36564  axextdist  36636  axextbdist  36637  nfwlim  36659  finminlem  37181  axtcond  37341  mh-inf3f1  37404  bj-dvelimdv  37838  bj-axreprepsep  38066  bj-opabco  38185  isbasisrelowllem1  38354  isbasisrelowllem2  38355  fvineqsneu  38410  fvineqsneq  38411  wl-cbvalnaed  38540  wl-2sb6d  38566  wl-sbalnae  38570  wl-mo2tf  38579  wl-eutf  38581  phpreu  38603  poimirlem26  38640  poimirlem27  38641  heicant  38649  mbfposadd  38661  ftc1anclem5  38691  indexdom  38744  filbcmb  38750  sdclem2  38752  sdclem1  38753  fdc1  38756  riotasv2d  40090  riotasv2s  40091  nfded2  40101  glbconxN  40511  pmapglb2xN  40905  cdlemefs32sn1aw  41547  mzpsubmpt  43830  mzpexpmpt  43832  eq0rabdioph  43863  eqrabdioph  43864  setindtr  44107  unielss  44296  nadd1suc  44470  ss2iundf  44735  mnuprdlem4  45335  ismnushort  45361  binomcxplemnotnn0  45416  iunconnlem2  45993  nfrelp  46015  modelaxreplem3  46046  modelaxrep  46047  permaxrep  46072  elunif  46109  rspcegf  46116  fnchoice  46122  refsumcn  46123  rfcnnnub  46129  uzwo4  46146  fiiuncl  46158  cbvmpo2  46188  cbvmpo1  46189  iinssiin  46220  disjf1  46274  disjrnmpt2  46279  disjf1o  46282  disjinfi  46283  choicefi  46290  axccdom  46311  dmrelrnrel  46315  axccd  46317  rnmptbddlem  46332  rnmptbd2lem  46336  infnsuprnmpt  46338  rnmptbdlem  46343  rnmptssbi  46348  upbdrech  46397  ssfiunibd  46401  supxrgere  46421  supxrgelem  46425  supxrge  46426  xralrple2  46442  infxr  46454  infxrunb2  46455  xrralrecnnle  46470  xrralrecnnge  46477  supxrunb3  46486  supxrleubrnmpt  46492  infleinf2  46500  unb2ltle  46501  rexabslelem  46504  suprleubrnmpt  46508  uzub  46517  supminfrnmpt  46531  supxrleubrnmptf  46537  infxrgelbrnmpt  46540  infrpgernmpt  46551  monoordxr  46568  monoord2xr  46570  caucvgbf  46575  cvgcaule  46577  iccshift  46606  iooshift  46610  iooiinicc  46630  iooiinioc  46644  fsummulc1f  46659  fsumf1of  46662  fsumreclf  46664  fsumlessf  46665  fmul01  46668  fmuldfeqlem1  46670  fmuldfeq  46671  fmul01lt1lem1  46672  fmul01lt1lem2  46673  fprodexp  46682  mccl  46686  fprodcnlem  46687  fprodcn  46688  climmulf  46692  climexp  46693  climsuse  46696  climrecf  46697  climinff  46699  climaddf  46703  mullimc  46704  islptre  46707  climf  46710  mullimcf  46711  rexlim2d  46713  idlimc  46714  limcperiod  46716  limcrecl  46717  islpcn  46725  limsupre  46727  limcleqr  46730  addlimc  46734  limclner  46737  climsubmpt  46746  climreclf  46750  climf2  46752  climeldmeqmpt  46754  clim2f2  46756  climfveqmpt  46757  fnlimfvre  46760  allbutfifvre  46761  climleltrp  46762  fnlimf  46764  fnlimabslt  46765  climfveqf  46766  climfveqmpt3  46768  climeldmeqf  46769  climeqf  46774  climeldmeqmpt3  46775  limsuppnfd  46788  limsupub  46790  climinf2lem  46792  climinf2  46793  limsuppnf  46797  limsupubuz  46799  climinf2mpt  46800  climinfmpt  46801  climinf3  46802  limsupmnflem  46806  limsupequz  46809  limsupre2  46811  limsupmnfuzlem  46812  limsupequzmptf  46817  limsupre3  46819  limsupre3uzlem  46821  limsupreuzmpt  46825  climisp  46832  lmbr3  46833  climrescn  46834  climxrrelem  46835  climxrre  46836  limsupub2  46898  liminflbuz2  46901  xlimmnfvlem2  46919  xlimmnfv  46920  xlimpnfvlem2  46923  xlimpnfv  46924  xlimmnfmpt  46929  xlimpnfmpt  46930  climxlim2lem  46931  cncficcgt0  46974  cncfioobd  46983  fprodsubrecnncnvlem  46993  fprodaddrecnncnvlem  46995  dvmptmulf  47023  dvnmul  47029  dvmptfprodlem  47030  dvmptfprod  47031  dvnprodlem1  47032  dvnprodlem2  47033  iblsplitf  47056  itgperiod  47067  stoweidlem3  47089  stoweidlem26  47112  stoweidlem27  47113  stoweidlem29  47115  stoweidlem31  47117  stoweidlem34  47120  stoweidlem35  47121  stoweidlem36  47122  stoweidlem39  47125  stoweidlem42  47128  stoweidlem43  47129  stoweidlem44  47130  stoweidlem46  47132  stoweidlem48  47134  stoweidlem49  47135  stoweidlem51  47137  stoweidlem52  47138  stoweidlem53  47139  stoweidlem54  47140  stoweidlem55  47141  stoweidlem56  47142  stoweidlem57  47143  stoweidlem58  47144  stoweidlem59  47145  stoweidlem60  47146  stoweidlem61  47147  stoweidlem62  47148  stoweid  47149  wallispilem3  47153  stirlinglem13  47172  stirling  47175  fourierdlem16  47209  fourierdlem21  47214  fourierdlem22  47215  fourierdlem31  47224  fourierdlem39  47232  fourierdlem48  47240  fourierdlem51  47243  fourierdlem68  47260  fourierdlem71  47263  fourierdlem73  47265  fourierdlem80  47272  fourierdlem81  47273  fourierdlem86  47278  fourierdlem87  47279  fourierdlem93  47285  fourierdlem94  47286  fourierdlem103  47295  fourierdlem104  47296  fourierdlem112  47304  fourierdlem113  47305  elaa2  47320  etransclem32  47352  salexct  47420  sge0revalmpt  47464  sge0f1o  47468  sge0lefi  47484  sge0resplit  47492  sge0lempt  47496  sge0iunmptlemre  47501  sge0fodjrnlem  47502  sge0iunmpt  47504  sge0ltfirpmpt2  47512  sge0isum  47513  sge0xp  47515  sge0isummpt2  47518  sge0xadd  47521  sge0pnffsumgt  47528  sge0gtfsumgt  47529  sge0uzfsumgt  47530  sge0reuz  47533  sge0reuzb  47534  iundjiun  47546  meadjiun  47552  ismeannd  47553  voliunsge0lem  47558  meaiunincf  47569  meaiuninc3v  47570  meaiuninc3  47571  meaiininc  47573  caragenfiiuncl  47601  omeiunltfirp  47605  ovnsubaddlem2  47657  hoidmvval0  47673  hoidmvlelem1  47681  hoidmvlelem3  47683  hoidmvlelem5  47685  ovnlecvr2  47696  hspdifhsp  47702  hoiqssbllem2  47709  hoiqssbllem3  47710  hspmbllem2  47713  opnvonmbllem2  47719  hoimbl2  47751  vonhoire  47758  iinhoiicc  47760  iunhoiioolem  47761  iunhoiioo  47762  vonioo  47768  vonicc  47771  vonn0ioo2  47776  vonn0icc2  47778  salpreimagelt  47793  salpreimalegt  47795  pimincfltioc  47802  pimdecfgtioo  47803  pimincfltioo  47804  preimageiingt  47806  preimaleiinlt  47807  salpreimagtge  47811  salpreimaltle  47812  salpreimalelt  47815  salpreimagtlt  47816  incsmflem  47827  issmflelem  47830  issmfle  47831  smfconst  47835  issmfgtlem  47841  issmfgt  47842  smfaddlem2  47850  smfadd  47851  decsmflem  47852  decsmf  47853  issmfgelem  47855  issmfge  47856  smflimlem2  47858  smflim  47863  smfresal  47874  smfrec  47875  smfmullem4  47880  smfmul  47881  smfpimcc  47894  smflimmpt  47896  smfsuplem1  47897  smfsupmpt  47901  smfsupxr  47902  smfinflem  47903  smfinfmpt  47905  smflimsuplem5  47910  smflimsuplem7  47912  smflimsuplem8  47913  smflimsupmpt  47915  smfliminflem  47916  smfliminfmpt  47918  smfpimne2  47926  fsupdm  47928  smfsupdmmbllem  47930  finfdm  47932  smfinfdmmbllem  47934  or2expropbilem2  48179  or2expropbi  48180  cfsetsnfsetf  48204  2reu8i  48259  nfdfat  48273  iccelpart  48591  ichnfim  48622  ich2exprop  48629  ichreuopeq  48631  sprsymrelfo  48655  reupr  48680  reuopreuprim  48684  2zrngmmgm  49425  cbvmpox2  49524  ovmpordxf  49527  1arymaptfo  49831  2arymaptfo  49842  iinfssclem3  50240  iinfssc  50241  iinfsubc  50242  pgindnf  50885  nfals  50975  nfrals  50976  nfalseu  51006  nfralseu  51007  aacllem  51015