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  5217  axrep4OLD  5220  axrep5  5221  reusv2lem3  5343  axprlem4OLD  5373  axprlem5OLD  5374  nfpo  5545  nfso  5546  nffr  5604  nfwe  5606  nfxp  5664  opeliunxp  5698  opeliun2xp  5699  nfco  5821  elrnmpt1  5916  nfimad  6035  reuop  6258  iota2  6488  nffun  6522  imadif  6583  nffn  6598  nff  6665  nff1  6735  nffo  6752  nff1o  6779  nffvd  6853  fv3  6859  funimassd  6907  fvmptdf  6955  fompt  7071  f1ossf1o  7082  fmptco  7083  fsnex  7238  nfiso  7277  nfriotadw  7332  cbvriotaw  7333  nfriotad  7335  cbvriota  7337  riota2df  7347  riota5f  7352  oprabv  7427  nfoprab  7431  mpoeq123  7439  nfmpo  7449  cbvoprab1  7454  cbvoprab2  7455  cbvoprab12  7456  cbvoprab3  7458  cbvmpox  7460  ovmpodxf  7517  elovmporab  7613  elovmporab1w  7614  elovmporab1  7615  onminex  7756  fiun  7896  f1iun  7897  opabex3d  7918  opabex3rd  7919  opabex3  7920  dfoprab4f  8009  fmpox  8020  opeliunxp2f  8160  nffrecs  8233  frrlem4  8239  tfr3  8338  tz7.49  8384  naddsuc2  8637  erovlem  8760  nfixpw  8864  nfixp  8865  nfixp1  8866  xpf1o  9077  nneneq  9140  ac6sfi  9194  nfoi  9429  wdom2d  9495  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  11309  dedekindle  11310  fsuppmapnn0fiublem  13952  fsuppmapnn0fiub  13953  fsuppmapnn0fiubex  13954  reuccatpfxs1  14709  nfsum1  15652  nfsum  15653  fsumclf  15700  fsumsplitf  15704  fsumsplit1  15707  fsum2dlem  15732  fsum00  15761  nfcprod1  15873  nfcprod  15874  fprod2dlem  15945  fprodsplitf  15953  fprodsplit1f  15955  fprodle  15961  lcmfunsnlem1  16606  lcmfunsnlem2lem1  16607  lcmfunsnlem2  16609  mreexexd  17614  acsmapd  18520  gsum2d2lem  19948  dprd2d2  20021  gsummoncoe1  22273  gsummatr01lem4  22623  cpmatmcllem  22683  cayleyhamilton1  22857  neiptopnei  23097  neiptopreu  23098  neitr  23145  iunconnlem  23392  iunconn  23393  ptcnplem  23586  ptcnp  23587  xkocnv  23779  isfildlem  23822  utopsnneiplem  24212  isucn2  24243  cfilucfil  24524  restmetu  24535  ovolfiniun  25468  ovoliunlem3  25471  ovoliunnul  25474  volfiniun  25514  itg2splitlem  25715  itg2split  25716  isibl2  25733  nfitg  25742  cbvitg  25743  limciun  25861  2sqmo  27400  2sqreulem4  27417  bdaypw2n0bndlem  28455  istrkg2ld  28528  chirred  32466  sbc2iedf  32534  rspc2daf  32535  opreu2reuALT  32546  mo5f  32558  foresf1o  32574  iinabrex  32639  cbvdisjf  32641  disjabrex  32652  disjabrexf  32653  funimass4f  32710  2ndresdju  32722  fmptcof2  32730  fcomptf  32731  acunirnmpt2  32733  acunirnmpt2f  32734  aciunf1lem  32735  funcnv4mpt  32741  fnpreimac  32743  f1od2  32792  fpwrelmap  32806  xrofsup  32840  nn0min  32894  fprodex01  32898  fsumiunle  32902  prodindf  32922  suppgsumssiun  33133  isarchiofld  33260  elrgspnsubrunlem2  33309  nsgqusf1olem1  33473  nsgqusf1olem3  33475  elrspunidl  33488  deg1prod  33643  mplvrpmga  33689  esplyfval1  33717  vieta  33724  fedgmullem2  33774  irngnzply1  33835  reff  33983  locfinreflem  33984  cmpcref  33994  zarclsiin  34015  zarcmplem  34025  ordtconnlem1  34068  esumcl  34174  gsumesum  34203  esumlub  34204  esumcst  34207  esumrnmpt2  34212  esumfzf  34213  esumfsup  34214  hasheuni  34229  esumcvg  34230  esumgect  34234  esumcvgre  34235  esum2dlem  34236  esum2d  34237  esumiun  34238  ldsysgenld  34304  sigapildsyslem  34305  sigapildsys  34306  ldgenpisyslem1  34307  measvunilem  34356  measvunilem0  34357  measvuni  34358  measinblem  34364  voliune  34373  volfiniune  34374  volmeas  34375  oms0  34441  omssubadd  34444  eulerpartlemgvv  34520  dstrvprob  34616  breprexplema  34774  bnj919  34910  bnj1146  34933  bnj1379  34972  bnj849  35067  bnj916  35075  bnj964  35085  bnj1014  35103  bnj1123  35128  bnj1228  35153  bnj1307  35165  bnj1321  35169  bnj1398  35176  bnj1408  35178  bnj1444  35185  bnj1445  35186  bnj1446  35187  bnj1449  35190  bnj1467  35196  bnj1463  35197  bnj1489  35198  bnj1491  35199  bnj1312  35200  bnj1525  35211  dvelimalcased  35217  dvelimexcased  35219  fineqvrep  35258  cvmcov  35445  iota5f  35906  axextdist  35979  axextbdist  35980  nfwlim  36002  finminlem  36500  axtcond  36660  bj-dvelimdv  37158  bj-axreprepsep  37382  bj-opabco  37502  isbasisrelowllem1  37671  isbasisrelowllem2  37672  fvineqsneu  37727  fvineqsneq  37728  wl-cbvalnaed  37857  wl-2sb6d  37883  wl-sbalnae  37887  wl-mo2tf  37896  wl-eutf  37898  phpreu  37925  poimirlem26  37967  poimirlem27  37968  heicant  37976  mbfposadd  37988  ftc1anclem5  38018  indexdom  38055  filbcmb  38061  sdclem2  38063  sdclem1  38064  fdc1  38067  riotasv2d  39403  riotasv2s  39404  nfded2  39414  glbconxN  39824  pmapglb2xN  40218  cdlemefs32sn1aw  40860  mzpsubmpt  43175  mzpexpmpt  43177  eq0rabdioph  43208  eqrabdioph  43209  setindtr  43452  unielss  43646  nadd1suc  43820  ss2iundf  44086  scottabf  44667  mnuprdlem4  44702  ismnushort  44728  binomcxplemnotnn0  44783  iunconnlem2  45361  nfrelp  45376  modelaxreplem3  45407  modelaxrep  45408  permaxrep  45433  elunif  45447  rspcegf  45454  fnchoice  45460  refsumcn  45461  rfcnnnub  45467  uzwo4  45484  fiiuncl  45496  cbvmpo2  45527  cbvmpo1  45528  iinssiin  45559  disjf1  45613  disjrnmpt2  45618  disjf1o  45621  disjinfi  45622  choicefi  45629  axccdom  45651  dmrelrnrel  45655  axccd  45658  rnmptbddlem  45673  rnmptbd2lem  45677  infnsuprnmpt  45679  rnmptbdlem  45684  rnmptssbi  45689  upbdrech  45738  ssfiunibd  45742  supxrgere  45763  supxrgelem  45767  supxrge  45768  xralrple2  45784  infxr  45796  infxrunb2  45797  xrralrecnnle  45812  xrralrecnnge  45819  supxrunb3  45828  supxrleubrnmpt  45834  infleinf2  45842  unb2ltle  45843  rexabslelem  45846  suprleubrnmpt  45850  uzub  45859  supminfrnmpt  45873  supxrleubrnmptf  45879  infxrgelbrnmpt  45882  infrpgernmpt  45893  monoordxr  45910  monoord2xr  45912  caucvgbf  45917  cvgcaule  45919  iccshift  45948  iooshift  45952  iooiinicc  45972  iooiinioc  45986  fsummulc1f  46001  fsumf1of  46004  fsumreclf  46006  fsumlessf  46007  fmul01  46010  fmuldfeqlem1  46012  fmuldfeq  46013  fmul01lt1lem1  46014  fmul01lt1lem2  46015  fprodexp  46024  mccl  46028  fprodcnlem  46029  fprodcn  46030  climmulf  46034  climexp  46035  climsuse  46038  climrecf  46039  climinff  46041  climaddf  46045  mullimc  46046  islptre  46049  climf  46052  mullimcf  46053  rexlim2d  46055  idlimc  46056  limcperiod  46058  limcrecl  46059  islpcn  46067  limsupre  46069  limcleqr  46072  addlimc  46076  limclner  46079  climsubmpt  46088  climreclf  46092  climf2  46094  climeldmeqmpt  46096  clim2f2  46098  climfveqmpt  46099  fnlimfvre  46102  allbutfifvre  46103  climleltrp  46104  fnlimf  46106  fnlimabslt  46107  climfveqf  46108  climfveqmpt3  46110  climeldmeqf  46111  climeqf  46116  climeldmeqmpt3  46117  limsuppnfd  46130  limsupub  46132  climinf2lem  46134  climinf2  46135  limsuppnf  46139  limsupubuz  46141  climinf2mpt  46142  climinfmpt  46143  climinf3  46144  limsupmnflem  46148  limsupequz  46151  limsupre2  46153  limsupmnfuzlem  46154  limsupequzmptf  46159  limsupre3  46161  limsupre3uzlem  46163  limsupreuzmpt  46167  climisp  46174  lmbr3  46175  climrescn  46176  climxrrelem  46177  climxrre  46178  limsupub2  46240  liminflbuz2  46243  xlimmnfvlem2  46261  xlimmnfv  46262  xlimpnfvlem2  46265  xlimpnfv  46266  xlimmnfmpt  46271  xlimpnfmpt  46272  climxlim2lem  46273  cncficcgt0  46316  cncfioobd  46325  fprodsubrecnncnvlem  46335  fprodaddrecnncnvlem  46337  dvmptmulf  46365  dvnmul  46371  dvmptfprodlem  46372  dvmptfprod  46373  dvnprodlem1  46374  dvnprodlem2  46375  iblsplitf  46398  itgperiod  46409  stoweidlem3  46431  stoweidlem26  46454  stoweidlem27  46455  stoweidlem29  46457  stoweidlem31  46459  stoweidlem34  46462  stoweidlem35  46463  stoweidlem36  46464  stoweidlem39  46467  stoweidlem42  46470  stoweidlem43  46471  stoweidlem44  46472  stoweidlem46  46474  stoweidlem48  46476  stoweidlem49  46477  stoweidlem51  46479  stoweidlem52  46480  stoweidlem53  46481  stoweidlem54  46482  stoweidlem55  46483  stoweidlem56  46484  stoweidlem57  46485  stoweidlem58  46486  stoweidlem59  46487  stoweidlem60  46488  stoweidlem61  46489  stoweidlem62  46490  stoweid  46491  wallispilem3  46495  stirlinglem13  46514  stirling  46517  fourierdlem16  46551  fourierdlem21  46556  fourierdlem22  46557  fourierdlem31  46566  fourierdlem39  46574  fourierdlem48  46582  fourierdlem51  46585  fourierdlem68  46602  fourierdlem71  46605  fourierdlem73  46607  fourierdlem80  46614  fourierdlem81  46615  fourierdlem86  46620  fourierdlem87  46621  fourierdlem93  46627  fourierdlem94  46628  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  fourierdlem113  46647  elaa2  46662  etransclem32  46694  salexct  46762  sge0revalmpt  46806  sge0f1o  46810  sge0lefi  46826  sge0resplit  46834  sge0lempt  46838  sge0iunmptlemre  46843  sge0fodjrnlem  46844  sge0iunmpt  46846  sge0ltfirpmpt2  46854  sge0isum  46855  sge0xp  46857  sge0isummpt2  46860  sge0xadd  46863  sge0pnffsumgt  46870  sge0gtfsumgt  46871  sge0uzfsumgt  46872  sge0reuz  46875  sge0reuzb  46876  iundjiun  46888  meadjiun  46894  ismeannd  46895  voliunsge0lem  46900  meaiunincf  46911  meaiuninc3v  46912  meaiuninc3  46913  meaiininc  46915  caragenfiiuncl  46943  omeiunltfirp  46947  ovnsubaddlem2  46999  hoidmvval0  47015  hoidmvlelem1  47023  hoidmvlelem3  47025  hoidmvlelem5  47027  ovnlecvr2  47038  hspdifhsp  47044  hoiqssbllem2  47051  hoiqssbllem3  47052  hspmbllem2  47055  opnvonmbllem2  47061  hoimbl2  47093  vonhoire  47100  iinhoiicc  47102  iunhoiioolem  47103  iunhoiioo  47104  vonioo  47110  vonicc  47113  vonn0ioo2  47118  vonn0icc2  47120  salpreimagelt  47135  salpreimalegt  47137  pimincfltioc  47144  pimdecfgtioo  47145  pimincfltioo  47146  preimageiingt  47148  preimaleiinlt  47149  salpreimagtge  47153  salpreimaltle  47154  salpreimalelt  47157  salpreimagtlt  47158  incsmflem  47169  issmflelem  47172  issmfle  47173  smfconst  47177  issmfgtlem  47183  issmfgt  47184  smfaddlem2  47192  smfadd  47193  decsmflem  47194  decsmf  47195  issmfgelem  47197  issmfge  47198  smflimlem2  47200  smflim  47205  smfresal  47216  smfrec  47217  smfmullem4  47222  smfmul  47223  smfpimcc  47236  smflimmpt  47238  smfsuplem1  47239  smfsupmpt  47243  smfsupxr  47244  smfinflem  47245  smfinfmpt  47247  smflimsuplem5  47252  smflimsuplem7  47254  smflimsuplem8  47255  smflimsupmpt  47257  smfliminflem  47258  smfliminfmpt  47260  smfpimne2  47268  fsupdm  47270  smfsupdmmbllem  47272  finfdm  47274  smfinfdmmbllem  47276  or2expropbilem2  47475  or2expropbi  47476  cfsetsnfsetf  47500  2reu8i  47555  nfdfat  47569  iccelpart  47887  ichnfim  47918  ich2exprop  47925  ichreuopeq  47927  sprsymrelfo  47951  reupr  47976  reuopreuprim  47980  2zrngmmgm  48722  cbvmpox2  48806  ovmpordxf  48809  1arymaptfo  49113  2arymaptfo  49124  iinfssclem3  49525  iinfssc  49526  iinfsubc  49527  setrec1  50160  pgindnf  50185  aacllem  50270