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  3340  cbvrmow  3368  nfrmow  3372  nfreuw  3373  cbvreu  3382  cbvrabw  3425  cbvrabwOLD  3426  nfrabw  3427  cbvrab  3429  ceqsex2  3482  vtocl2gafOLD  3524  vtocl3gaf  3525  spc2ed  3544  rspce  3554  eqvincf  3593  elrabf  3632  elrab3t  3634  rexab2  3646  morex  3666  reu2  3672  rmo3f  3681  reu2eqd  3683  sbc2iegf  3804  reu8nf  3816  rmo2  3826  rmo3  3828  csbiebt  3867  csbie2t  3876  cbvrabcsfw  3879  cbvreucsf  3882  cbvrabcsf  3883  nfdif  4070  nfin  4165  reusngf  4619  rexreusng  4624  reuprg0  4647  rabsnifsb  4667  nfop  4833  nfopd  4834  eluniab  4865  iuneqconst  4946  cbvopab  5158  cbvopab1  5160  cbvopab1g  5161  cbvopab2  5162  cbvopab1s  5163  mpteq12f  5171  nfmpt  5184  cbvmptf  5186  cbvmptfg  5187  axrep3  5216  axrep4OLD  5219  axrep5  5220  reusv2lem3  5335  axprlem4OLD  5365  axprlem5OLD  5366  nfpo  5536  nfso  5537  nffr  5595  nfwe  5597  nfxp  5655  opeliunxp  5689  opeliun2xp  5690  nfco  5812  elrnmpt1  5907  nfimad  6026  reuop  6249  iota2  6479  nffun  6513  imadif  6574  nffn  6589  nff  6656  nff1  6726  nffo  6743  nff1o  6770  nffvd  6844  fv3  6850  funimassd  6898  fvmptdf  6946  fompt  7062  f1ossf1o  7073  fmptco  7074  fsnex  7229  nfiso  7268  nfriotadw  7323  cbvriotaw  7324  nfriotad  7326  cbvriota  7328  riota2df  7338  riota5f  7343  oprabv  7418  nfoprab  7422  mpoeq123  7430  nfmpo  7440  cbvoprab1  7445  cbvoprab2  7446  cbvoprab12  7447  cbvoprab3  7449  cbvmpox  7451  ovmpodxf  7508  elovmporab  7604  elovmporab1w  7605  elovmporab1  7606  onminex  7747  fiun  7887  f1iun  7888  opabex3d  7909  opabex3rd  7910  opabex3  7911  dfoprab4f  8000  fmpox  8011  opeliunxp2f  8151  nffrecs  8224  frrlem4  8230  tfr3  8329  tz7.49  8375  naddsuc2  8628  erovlem  8751  nfixpw  8855  nfixp  8856  nfixp1  8857  xpf1o  9068  nneneq  9131  ac6sfi  9185  nfoi  9420  wdom2d  9486  infpssrlem4  10217  hsmexlem2  10338  hsmexlem4  10340  domtriomlem  10353  axdc3lem2  10362  axdc4lem  10366  zorn2lem4  10410  zorn2lem5  10411  konigthlem  10480  axextnd  10503  axrepndlem2  10505  axrepnd  10506  axunnd  10508  axpowndlem2  10510  axpowndlem4  10512  axpownd  10513  axregndlem2  10515  axregnd  10516  axinfndlem1  10517  axinfnd  10518  zfcndrep  10526  zfcndinf  10530  dedekind  11298  dedekindle  11299  fsuppmapnn0fiublem  13941  fsuppmapnn0fiub  13942  fsuppmapnn0fiubex  13943  reuccatpfxs1  14698  nfsum1  15641  nfsum  15642  fsumclf  15689  fsumsplitf  15693  fsumsplit1  15696  fsum2dlem  15721  fsum00  15750  nfcprod1  15862  nfcprod  15863  fprod2dlem  15934  fprodsplitf  15942  fprodsplit1f  15944  fprodle  15950  lcmfunsnlem1  16595  lcmfunsnlem2lem1  16596  lcmfunsnlem2  16598  mreexexd  17603  acsmapd  18509  gsum2d2lem  19937  dprd2d2  20010  gsummoncoe1  22282  gsummatr01lem4  22632  cpmatmcllem  22692  cayleyhamilton1  22866  neiptopnei  23106  neiptopreu  23107  neitr  23154  iunconnlem  23401  iunconn  23402  ptcnplem  23595  ptcnp  23596  xkocnv  23788  isfildlem  23831  utopsnneiplem  24221  isucn2  24252  cfilucfil  24533  restmetu  24544  ovolfiniun  25477  ovoliunlem3  25480  ovoliunnul  25483  volfiniun  25523  itg2splitlem  25724  itg2split  25725  isibl2  25742  nfitg  25751  cbvitg  25752  limciun  25870  2sqmo  27419  2sqreulem4  27436  bdaypw2n0bndlem  28474  istrkg2ld  28547  chirred  32486  sbc2iedf  32554  rspc2daf  32555  opreu2reuALT  32566  mo5f  32578  foresf1o  32594  iinabrex  32659  cbvdisjf  32661  disjabrex  32672  disjabrexf  32673  funimass4f  32730  2ndresdju  32742  fmptcof2  32750  fcomptf  32751  acunirnmpt2  32753  acunirnmpt2f  32754  aciunf1lem  32755  funcnv4mpt  32761  fnpreimac  32763  f1od2  32812  fpwrelmap  32826  xrofsup  32860  nn0min  32914  fprodex01  32918  fsumiunle  32922  prodindf  32942  suppgsumssiun  33153  isarchiofld  33280  elrgspnsubrunlem2  33329  nsgqusf1olem1  33493  nsgqusf1olem3  33495  elrspunidl  33508  deg1prod  33663  mplvrpmga  33709  esplyfval1  33737  vieta  33744  fedgmullem2  33795  irngnzply1  33856  reff  34004  locfinreflem  34005  cmpcref  34015  zarclsiin  34036  zarcmplem  34046  ordtconnlem1  34089  esumcl  34195  gsumesum  34224  esumlub  34225  esumcst  34228  esumrnmpt2  34233  esumfzf  34234  esumfsup  34235  hasheuni  34250  esumcvg  34251  esumgect  34255  esumcvgre  34256  esum2dlem  34257  esum2d  34258  esumiun  34259  ldsysgenld  34325  sigapildsyslem  34326  sigapildsys  34327  ldgenpisyslem1  34328  measvunilem  34377  measvunilem0  34378  measvuni  34379  measinblem  34385  voliune  34394  volfiniune  34395  volmeas  34396  oms0  34462  omssubadd  34465  eulerpartlemgvv  34541  dstrvprob  34637  breprexplema  34795  bnj919  34931  bnj1146  34954  bnj1379  34993  bnj849  35088  bnj916  35096  bnj964  35106  bnj1014  35124  bnj1123  35149  bnj1228  35174  bnj1307  35186  bnj1321  35190  bnj1398  35197  bnj1408  35199  bnj1444  35206  bnj1445  35207  bnj1446  35208  bnj1449  35211  bnj1467  35217  bnj1463  35218  bnj1489  35219  bnj1491  35220  bnj1312  35221  bnj1525  35232  dvelimalcased  35238  dvelimexcased  35240  fineqvrep  35279  cvmcov  35466  iota5f  35927  axextdist  36000  axextbdist  36001  nfwlim  36023  finminlem  36521  axtcond  36681  bj-dvelimdv  37171  bj-axreprepsep  37395  bj-opabco  37515  isbasisrelowllem1  37682  isbasisrelowllem2  37683  fvineqsneu  37738  fvineqsneq  37739  wl-cbvalnaed  37868  wl-2sb6d  37894  wl-sbalnae  37898  wl-mo2tf  37907  wl-eutf  37909  phpreu  37936  poimirlem26  37978  poimirlem27  37979  heicant  37987  mbfposadd  37999  ftc1anclem5  38029  indexdom  38066  filbcmb  38072  sdclem2  38074  sdclem1  38075  fdc1  38078  riotasv2d  39414  riotasv2s  39415  nfded2  39425  glbconxN  39835  pmapglb2xN  40229  cdlemefs32sn1aw  40871  mzpsubmpt  43186  mzpexpmpt  43188  eq0rabdioph  43219  eqrabdioph  43220  setindtr  43467  unielss  43661  nadd1suc  43835  ss2iundf  44101  scottabf  44682  mnuprdlem4  44717  ismnushort  44743  binomcxplemnotnn0  44798  iunconnlem2  45376  nfrelp  45391  modelaxreplem3  45422  modelaxrep  45423  permaxrep  45448  elunif  45462  rspcegf  45469  fnchoice  45475  refsumcn  45476  rfcnnnub  45482  uzwo4  45499  fiiuncl  45511  cbvmpo2  45542  cbvmpo1  45543  iinssiin  45574  disjf1  45628  disjrnmpt2  45633  disjf1o  45636  disjinfi  45637  choicefi  45644  axccdom  45666  dmrelrnrel  45670  axccd  45673  rnmptbddlem  45688  rnmptbd2lem  45692  infnsuprnmpt  45694  rnmptbdlem  45699  rnmptssbi  45704  upbdrech  45753  ssfiunibd  45757  supxrgere  45778  supxrgelem  45782  supxrge  45783  xralrple2  45799  infxr  45811  infxrunb2  45812  xrralrecnnle  45827  xrralrecnnge  45834  supxrunb3  45843  supxrleubrnmpt  45849  infleinf2  45857  unb2ltle  45858  rexabslelem  45861  suprleubrnmpt  45865  uzub  45874  supminfrnmpt  45888  supxrleubrnmptf  45894  infxrgelbrnmpt  45897  infrpgernmpt  45908  monoordxr  45925  monoord2xr  45927  caucvgbf  45932  cvgcaule  45934  iccshift  45963  iooshift  45967  iooiinicc  45987  iooiinioc  46001  fsummulc1f  46016  fsumf1of  46019  fsumreclf  46021  fsumlessf  46022  fmul01  46025  fmuldfeqlem1  46027  fmuldfeq  46028  fmul01lt1lem1  46029  fmul01lt1lem2  46030  fprodexp  46039  mccl  46043  fprodcnlem  46044  fprodcn  46045  climmulf  46049  climexp  46050  climsuse  46053  climrecf  46054  climinff  46056  climaddf  46060  mullimc  46061  islptre  46064  climf  46067  mullimcf  46068  rexlim2d  46070  idlimc  46071  limcperiod  46073  limcrecl  46074  islpcn  46082  limsupre  46084  limcleqr  46087  addlimc  46091  limclner  46094  climsubmpt  46103  climreclf  46107  climf2  46109  climeldmeqmpt  46111  clim2f2  46113  climfveqmpt  46114  fnlimfvre  46117  allbutfifvre  46118  climleltrp  46119  fnlimf  46121  fnlimabslt  46122  climfveqf  46123  climfveqmpt3  46125  climeldmeqf  46126  climeqf  46131  climeldmeqmpt3  46132  limsuppnfd  46145  limsupub  46147  climinf2lem  46149  climinf2  46150  limsuppnf  46154  limsupubuz  46156  climinf2mpt  46157  climinfmpt  46158  climinf3  46159  limsupmnflem  46163  limsupequz  46166  limsupre2  46168  limsupmnfuzlem  46169  limsupequzmptf  46174  limsupre3  46176  limsupre3uzlem  46178  limsupreuzmpt  46182  climisp  46189  lmbr3  46190  climrescn  46191  climxrrelem  46192  climxrre  46193  limsupub2  46255  liminflbuz2  46258  xlimmnfvlem2  46276  xlimmnfv  46277  xlimpnfvlem2  46280  xlimpnfv  46281  xlimmnfmpt  46286  xlimpnfmpt  46287  climxlim2lem  46288  cncficcgt0  46331  cncfioobd  46340  fprodsubrecnncnvlem  46350  fprodaddrecnncnvlem  46352  dvmptmulf  46380  dvnmul  46386  dvmptfprodlem  46387  dvmptfprod  46388  dvnprodlem1  46389  dvnprodlem2  46390  iblsplitf  46413  itgperiod  46424  stoweidlem3  46446  stoweidlem26  46469  stoweidlem27  46470  stoweidlem29  46472  stoweidlem31  46474  stoweidlem34  46477  stoweidlem35  46478  stoweidlem36  46479  stoweidlem39  46482  stoweidlem42  46485  stoweidlem43  46486  stoweidlem44  46487  stoweidlem46  46489  stoweidlem48  46491  stoweidlem49  46492  stoweidlem51  46494  stoweidlem52  46495  stoweidlem53  46496  stoweidlem54  46497  stoweidlem55  46498  stoweidlem56  46499  stoweidlem57  46500  stoweidlem58  46501  stoweidlem59  46502  stoweidlem60  46503  stoweidlem61  46504  stoweidlem62  46505  stoweid  46506  wallispilem3  46510  stirlinglem13  46529  stirling  46532  fourierdlem16  46566  fourierdlem21  46571  fourierdlem22  46572  fourierdlem31  46581  fourierdlem39  46589  fourierdlem48  46597  fourierdlem51  46600  fourierdlem68  46617  fourierdlem71  46620  fourierdlem73  46622  fourierdlem80  46629  fourierdlem81  46630  fourierdlem86  46635  fourierdlem87  46636  fourierdlem93  46642  fourierdlem94  46643  fourierdlem103  46652  fourierdlem104  46653  fourierdlem112  46661  fourierdlem113  46662  elaa2  46677  etransclem32  46709  salexct  46777  sge0revalmpt  46821  sge0f1o  46825  sge0lefi  46841  sge0resplit  46849  sge0lempt  46853  sge0iunmptlemre  46858  sge0fodjrnlem  46859  sge0iunmpt  46861  sge0ltfirpmpt2  46869  sge0isum  46870  sge0xp  46872  sge0isummpt2  46875  sge0xadd  46878  sge0pnffsumgt  46885  sge0gtfsumgt  46886  sge0uzfsumgt  46887  sge0reuz  46890  sge0reuzb  46891  iundjiun  46903  meadjiun  46909  ismeannd  46910  voliunsge0lem  46915  meaiunincf  46926  meaiuninc3v  46927  meaiuninc3  46928  meaiininc  46930  caragenfiiuncl  46958  omeiunltfirp  46962  ovnsubaddlem2  47014  hoidmvval0  47030  hoidmvlelem1  47038  hoidmvlelem3  47040  hoidmvlelem5  47042  ovnlecvr2  47053  hspdifhsp  47059  hoiqssbllem2  47066  hoiqssbllem3  47067  hspmbllem2  47070  opnvonmbllem2  47076  hoimbl2  47108  vonhoire  47115  iinhoiicc  47117  iunhoiioolem  47118  iunhoiioo  47119  vonioo  47125  vonicc  47128  vonn0ioo2  47133  vonn0icc2  47135  salpreimagelt  47150  salpreimalegt  47152  pimincfltioc  47159  pimdecfgtioo  47160  pimincfltioo  47161  preimageiingt  47163  preimaleiinlt  47164  salpreimagtge  47168  salpreimaltle  47169  salpreimalelt  47172  salpreimagtlt  47173  incsmflem  47184  issmflelem  47187  issmfle  47188  smfconst  47192  issmfgtlem  47198  issmfgt  47199  smfaddlem2  47207  smfadd  47208  decsmflem  47209  decsmf  47210  issmfgelem  47212  issmfge  47213  smflimlem2  47215  smflim  47220  smfresal  47231  smfrec  47232  smfmullem4  47237  smfmul  47238  smfpimcc  47251  smflimmpt  47253  smfsuplem1  47254  smfsupmpt  47258  smfsupxr  47259  smfinflem  47260  smfinfmpt  47262  smflimsuplem5  47267  smflimsuplem7  47269  smflimsuplem8  47270  smflimsupmpt  47272  smfliminflem  47273  smfliminfmpt  47275  smfpimne2  47283  fsupdm  47285  smfsupdmmbllem  47287  finfdm  47289  smfinfdmmbllem  47291  or2expropbilem2  47478  or2expropbi  47479  cfsetsnfsetf  47503  2reu8i  47558  nfdfat  47572  iccelpart  47890  ichnfim  47921  ich2exprop  47928  ichreuopeq  47930  sprsymrelfo  47954  reupr  47979  reuopreuprim  47983  2zrngmmgm  48725  cbvmpox2  48809  ovmpordxf  48812  1arymaptfo  49116  2arymaptfo  49127  iinfssclem3  49528  iinfssc  49529  iinfsubc  49530  setrec1  50163  pgindnf  50188  aacllem  50273