Theorem nfan 1928

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

This proof depends on syntax axioms:   ∧ wa 400  ⊤wtru 1570  Ⅎwnf 1812

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

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1572  df-ex 1809  df-nf 1813

This theorem is used by:  nfnan  1929  nf3an  1930  hban  2334  nfeqf  2412  nfald2  2476  2ax6elem  2501  nfsb4t  2530  nfeu1  2616  eupicka  2661  mopick2  2664  2mo  2675  nfabd2  2947  2ralbida  3287  r19.12  3313  reean  3314  ralcom2  3365  cbvrmow  3393  nfrmow  3397  nfreuw  3398  cbvreu  3407  cbvrabw  3450  nfrabw  3451  cbvrab  3453  ceqsex2  3504  vtocl3gaf  3543  spc2ed  3559  rspce  3569  eqvincf  3608  elrabf  3646  elrab3t  3648  rexab2  3661  morex  3681  reu2  3687  rmo3f  3696  reu2eqd  3698  sbc2iegf  3817  reu8nf  3829  rmo2  3839  rmo3  3841  csbiebt  3881  csbie2t  3890  cbvrabcsfw  3893  cbvreucsf  3896  cbvrabcsf  3897  nfdif  4083  nfin  4176  reusngf  4639  rexreusng  4644  reuprg0  4667  rabsnifsb  4687  nfop  4853  nfopd  4854  eluniab  4885  iuneqconst  4967  cbvopab  5182  cbvopab1  5184  cbvopab1g  5185  cbvopab2  5186  cbvopab1s  5187  mpteq12f  5195  nfmpt  5208  cbvmptf  5210  cbvmptfg  5211  axrep3  5241  axrep4OLD  5244  axrep5  5245  reusv2lem3  5370  axprlem4OLD  5400  axprlem5OLD  5401  nfpo  5574  nfso  5575  nffr  5633  nfwe  5635  nfxp  5693  opeliunxp  5727  opeliun2xp  5728  nfco  5850  elrnmpt1  5949  nfimad  6070  reuop  6294  iota2  6525  nffun  6559  imadif  6620  nffn  6634  nff  6701  nff1  6772  nffo  6791  nff1o  6818  nffvd  6893  fv3  6899  funimassd  6947  fvmptdf  6996  fompt  7113  f1ossf1o  7124  fmptco  7125  fsnex  7281  nfiso  7320  nfriotadw  7377  cbvriotaw  7378  nfriotad  7380  cbvriota  7382  riota2df  7392  riota5f  7397  oprabv  7472  nfoprab  7476  mpoeq123  7484  nfmpo  7494  cbvoprab1  7499  cbvoprab2  7500  cbvoprab12  7501  cbvoprab3  7503  cbvmpox  7505  ovmpodxf  7562  elovmporab  7658  elovmporab1w  7659  elovmporab1  7660  onminex  7799  fiun  7938  f1iun  7939  opabex3d  7960  opabex3rd  7961  opabex3  7962  dfoprab4f  8051  fmpox  8062  opeliunxp2f  8204  nffrecs  8278  frrlem4  8284  tfr3  8384  tz7.49  8430  naddsuc2  8686  erovlem  8809  nfixpw  8912  nfixp  8913  nfixp1  8914  xpf1o  9125  nneneq  9188  ac6sfi  9242  nfoi  9474  wdom2d  9540  scottabf  9866  infpssrlem4  10296  hsmexlem2  10417  hsmexlem4  10419  domtriomlem  10432  axdc3lem2  10441  axdc4lem  10445  zorn2lem4  10489  zorn2lem5  10490  konigthlem  10559  axextnd  10582  axrepndlem2  10584  axrepnd  10585  axunnd  10587  axpowndlem2  10589  axpowndlem4  10591  axpownd  10592  axregndlem2  10594  axregnd  10595  axinfndlem1  10596  axinfnd  10597  zfcndrep  10605  zfcndinf  10609  dedekind  11379  dedekindle  11380  fsuppmapnn0fiublem  14033  fsuppmapnn0fiub  14034  fsuppmapnn0fiubex  14035  reuccatpfxs1  14791  nfsum1  15748  nfsum  15749  fsumclf  15796  fsumsplitf  15800  fsumsplit1  15803  fsum2dlem  15828  fsum00  15857  nfcprod1  15969  nfcprod  15970  fprod2dlem  16041  fprodsplitf  16049  fprodsplit1f  16051  fprodle  16057  lcmfunsnlem1  16701  lcmfunsnlem2lem1  16702  lcmfunsnlem2  16704  mreexexd  17710  acsmapd  18616  gsum2d2lem  20049  dprd2d2  20122  gsummoncoe1  22479  gsummatr01lem4  22826  cpmatmcllem  22886  cayleyhamilton1  23060  neiptopnei  23300  neiptopreu  23301  neitr  23348  iunconnlem  23595  iunconn  23596  ptcnplem  23789  ptcnp  23790  xkocnv  23982  isfildlem  24025  utopsnneiplem  24415  isucn2  24446  cfilucfil  24727  restmetu  24738  ovolfiniun  25671  ovoliunlem3  25674  ovoliunnul  25677  volfiniun  25717  itg2splitlem  25918  itg2split  25919  isibl2  25936  nfitg  25945  cbvitg  25946  limciun  26064  2sqmo  27612  2sqreulem4  27629  bdaypw2n0bndlem  28667  istrkg2ld  28740  chirred  32758  sbc2iedf  32823  rspc2daf  32824  opreu2reuALT  32834  mo5f  32846  foresf1o  32861  iinabrex  32925  cbvdisjf  32927  disjabrex  32938  disjabrexf  32939  funimass4f  32993  2ndresdju  33005  fmptcof2  33013  fcomptf  33014  acunirnmpt2  33016  acunirnmpt2f  33017  aciunf1lem  33018  funcnv4mpt  33024  fnpreimac  33026  f1od2  33075  fpwrelmap  33089  xrofsup  33123  nn0min  33176  fprodex01  33180  fsumiunle  33184  prodindf  33193  suppgsumssiun  33401  isarchiofld  33528  elrgspnsubrunlem2  33577  nsgqusf1olem1  33731  nsgqusf1olem3  33733  elrspunidl  33745  deg1prod  33882  mplvrpmga  33944  esplyfval1  33972  vieta  33979  fedgmullem2  34029  irngnzply1  34090  reff  34238  locfinreflem  34239  cmpcref  34249  zarclsiin  34270  zarcmplem  34280  ordtconnlem1  34323  esumcl  34429  gsumesum  34458  esumlub  34459  esumcst  34462  esumrnmpt2  34467  esumfzf  34468  esumfsup  34469  hasheuni  34484  esumcvg  34485  esumgect  34489  esumcvgre  34490  esum2dlem  34491  esum2d  34492  esumiun  34493  ldsysgenld  34559  sigapildsyslem  34560  sigapildsys  34561  ldgenpisyslem1  34562  measvunilem  34611  measvunilem0  34612  measvuni  34613  measinblem  34619  voliune  34628  volfiniune  34629  volmeas  34630  oms0  34696  omssubadd  34699  eulerpartlemgvv  34775  dstrvprob  34871  breprexplema  35026  bnj919  35165  bnj1146  35188  bnj1379  35227  bnj849  35322  bnj916  35330  bnj964  35340  bnj1014  35358  bnj1123  35383  bnj1228  35408  bnj1307  35420  bnj1321  35424  bnj1398  35431  bnj1408  35433  bnj1444  35440  bnj1445  35441  bnj1446  35442  bnj1449  35445  bnj1467  35451  bnj1463  35452  bnj1489  35453  bnj1491  35454  bnj1312  35455  bnj1525  35466  dvelimalcased  35472  dvelimexcased  35474  fineqvrep  35535  cvmcov  35763  iota5f  36224  axextdist  36297  axextbdist  36298  nfwlim  36320  finminlem  36857  axtcond  37017  bj-dvelimdv  37514  bj-axreprepsep  37740  bj-opabco  37860  isbasisrelowllem1  38029  isbasisrelowllem2  38030  fvineqsneu  38085  fvineqsneq  38086  wl-cbvalnaed  38215  wl-2sb6d  38241  wl-sbalnae  38245  wl-mo2tf  38254  wl-eutf  38256  phpreu  38283  poimirlem26  38325  poimirlem27  38326  heicant  38334  mbfposadd  38346  ftc1anclem5  38376  indexdom  38413  filbcmb  38419  sdclem2  38421  sdclem1  38422  fdc1  38425  riotasv2d  39759  riotasv2s  39760  nfded2  39770  glbconxN  40180  pmapglb2xN  40574  cdlemefs32sn1aw  41216  mzpsubmpt  43502  mzpexpmpt  43504  eq0rabdioph  43535  eqrabdioph  43536  setindtr  43779  unielss  43973  nadd1suc  44147  ss2iundf  44413  mnuprdlem4  45013  ismnushort  45039  binomcxplemnotnn0  45094  iunconnlem2  45671  nfrelp  45686  modelaxreplem3  45717  modelaxrep  45718  permaxrep  45743  elunif  45764  rspcegf  45771  fnchoice  45777  refsumcn  45778  rfcnnnub  45784  uzwo4  45801  fiiuncl  45813  cbvmpo2  45843  cbvmpo1  45844  iinssiin  45875  disjf1  45929  disjrnmpt2  45934  disjf1o  45937  disjinfi  45938  choicefi  45945  axccdom  45966  dmrelrnrel  45970  axccd  45972  rnmptbddlem  45987  rnmptbd2lem  45991  infnsuprnmpt  45993  rnmptbdlem  45998  rnmptssbi  46003  upbdrech  46052  ssfiunibd  46056  supxrgere  46077  supxrgelem  46081  supxrge  46082  xralrple2  46098  infxr  46110  infxrunb2  46111  xrralrecnnle  46126  xrralrecnnge  46133  supxrunb3  46142  supxrleubrnmpt  46148  infleinf2  46156  unb2ltle  46157  rexabslelem  46160  suprleubrnmpt  46164  uzub  46173  supminfrnmpt  46187  supxrleubrnmptf  46193  infxrgelbrnmpt  46196  infrpgernmpt  46207  monoordxr  46224  monoord2xr  46226  caucvgbf  46231  cvgcaule  46233  iccshift  46262  iooshift  46266  iooiinicc  46286  iooiinioc  46300  fsummulc1f  46315  fsumf1of  46318  fsumreclf  46320  fsumlessf  46321  fmul01  46324  fmuldfeqlem1  46326  fmuldfeq  46327  fmul01lt1lem1  46328  fmul01lt1lem2  46329  fprodexp  46338  mccl  46342  fprodcnlem  46343  fprodcn  46344  climmulf  46348  climexp  46349  climsuse  46352  climrecf  46353  climinff  46355  climaddf  46359  mullimc  46360  islptre  46363  climf  46366  mullimcf  46367  rexlim2d  46369  idlimc  46370  limcperiod  46372  limcrecl  46373  islpcn  46381  limsupre  46383  limcleqr  46386  addlimc  46390  limclner  46393  climsubmpt  46402  climreclf  46406  climf2  46408  climeldmeqmpt  46410  clim2f2  46412  climfveqmpt  46413  fnlimfvre  46416  allbutfifvre  46417  climleltrp  46418  fnlimf  46420  fnlimabslt  46421  climfveqf  46422  climfveqmpt3  46424  climeldmeqf  46425  climeqf  46430  climeldmeqmpt3  46431  limsuppnfd  46444  limsupub  46446  climinf2lem  46448  climinf2  46449  limsuppnf  46453  limsupubuz  46455  climinf2mpt  46456  climinfmpt  46457  climinf3  46458  limsupmnflem  46462  limsupequz  46465  limsupre2  46467  limsupmnfuzlem  46468  limsupequzmptf  46473  limsupre3  46475  limsupre3uzlem  46477  limsupreuzmpt  46481  climisp  46488  lmbr3  46489  climrescn  46490  climxrrelem  46491  climxrre  46492  limsupub2  46554  liminflbuz2  46557  xlimmnfvlem2  46575  xlimmnfv  46576  xlimpnfvlem2  46579  xlimpnfv  46580  xlimmnfmpt  46585  xlimpnfmpt  46586  climxlim2lem  46587  cncficcgt0  46630  cncfioobd  46639  fprodsubrecnncnvlem  46649  fprodaddrecnncnvlem  46651  dvmptmulf  46679  dvnmul  46685  dvmptfprodlem  46686  dvmptfprod  46687  dvnprodlem1  46688  dvnprodlem2  46689  iblsplitf  46712  itgperiod  46723  stoweidlem3  46745  stoweidlem26  46768  stoweidlem27  46769  stoweidlem29  46771  stoweidlem31  46773  stoweidlem34  46776  stoweidlem35  46777  stoweidlem36  46778  stoweidlem39  46781  stoweidlem42  46784  stoweidlem43  46785  stoweidlem44  46786  stoweidlem46  46788  stoweidlem48  46790  stoweidlem49  46791  stoweidlem51  46793  stoweidlem52  46794  stoweidlem53  46795  stoweidlem54  46796  stoweidlem55  46797  stoweidlem56  46798  stoweidlem57  46799  stoweidlem58  46800  stoweidlem59  46801  stoweidlem60  46802  stoweidlem61  46803  stoweidlem62  46804  stoweid  46805  wallispilem3  46809  stirlinglem13  46828  stirling  46831  fourierdlem16  46865  fourierdlem21  46870  fourierdlem22  46871  fourierdlem31  46880  fourierdlem39  46888  fourierdlem48  46896  fourierdlem51  46899  fourierdlem68  46916  fourierdlem71  46919  fourierdlem73  46921  fourierdlem80  46928  fourierdlem81  46929  fourierdlem86  46934  fourierdlem87  46935  fourierdlem93  46941  fourierdlem94  46942  fourierdlem103  46951  fourierdlem104  46952  fourierdlem112  46960  fourierdlem113  46961  elaa2  46976  etransclem32  47008  salexct  47076  sge0revalmpt  47120  sge0f1o  47124  sge0lefi  47140  sge0resplit  47148  sge0lempt  47152  sge0iunmptlemre  47157  sge0fodjrnlem  47158  sge0iunmpt  47160  sge0ltfirpmpt2  47168  sge0isum  47169  sge0xp  47171  sge0isummpt2  47174  sge0xadd  47177  sge0pnffsumgt  47184  sge0gtfsumgt  47185  sge0uzfsumgt  47186  sge0reuz  47189  sge0reuzb  47190  iundjiun  47202  meadjiun  47208  ismeannd  47209  voliunsge0lem  47214  meaiunincf  47225  meaiuninc3v  47226  meaiuninc3  47227  meaiininc  47229  caragenfiiuncl  47257  omeiunltfirp  47261  ovnsubaddlem2  47313  hoidmvval0  47329  hoidmvlelem1  47337  hoidmvlelem3  47339  hoidmvlelem5  47341  ovnlecvr2  47352  hspdifhsp  47358  hoiqssbllem2  47365  hoiqssbllem3  47366  hspmbllem2  47369  opnvonmbllem2  47375  hoimbl2  47407  vonhoire  47414  iinhoiicc  47416  iunhoiioolem  47417  iunhoiioo  47418  vonioo  47424  vonicc  47427  vonn0ioo2  47432  vonn0icc2  47434  salpreimagelt  47449  salpreimalegt  47451  pimincfltioc  47458  pimdecfgtioo  47459  pimincfltioo  47460  preimageiingt  47462  preimaleiinlt  47463  salpreimagtge  47467  salpreimaltle  47468  salpreimalelt  47471  salpreimagtlt  47472  incsmflem  47483  issmflelem  47486  issmfle  47487  smfconst  47491  issmfgtlem  47497  issmfgt  47498  smfaddlem2  47506  smfadd  47507  decsmflem  47508  decsmf  47509  issmfgelem  47511  issmfge  47512  smflimlem2  47514  smflim  47519  smfresal  47530  smfrec  47531  smfmullem4  47536  smfmul  47537  smfpimcc  47550  smflimmpt  47552  smfsuplem1  47553  smfsupmpt  47557  smfsupxr  47558  smfinflem  47559  smfinfmpt  47561  smflimsuplem5  47566  smflimsuplem7  47568  smflimsuplem8  47569  smflimsupmpt  47571  smfliminflem  47572  smfliminfmpt  47574  smfpimne2  47582  fsupdm  47584  smfsupdmmbllem  47586  finfdm  47588  smfinfdmmbllem  47590  or2expropbilem2  47798  or2expropbi  47799  cfsetsnfsetf  47823  2reu8i  47878  nfdfat  47892  iccelpart  48210  ichnfim  48241  ich2exprop  48248  ichreuopeq  48250  sprsymrelfo  48274  reupr  48299  reuopreuprim  48303  2zrngmmgm  49045  cbvmpox2  49144  ovmpordxf  49147  1arymaptfo  49451  2arymaptfo  49462  iinfssclem3  49862  iinfssc  49863  iinfsubc  49864  setrec1  50497  pgindnf  50522  nfals  50609  nfrals  50610  nfalseu  50640  nfralseu  50641  aacllem  50649