Theorem nfan 1899

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

Syntax hints:   ∧ wa 395  ⊤wtru 1541  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfnan  1900  nf3an  1901  hban  2300  nfeqf  2380  nfald2  2444  2ax6elem  2469  nfsb4t  2498  nfeu1ALT  2583  eupicka  2628  mopick2  2631  2mo  2642  nfabd2  2916  2ralbida  3261  r19.12  3290  reean  3291  ralcom2  3353  cbvrmow  3383  nfrmow  3387  nfreuw  3388  cbvreuwOLD  3389  cbvreu  3400  cbvrabw  3444  cbvrabwOLD  3445  nfrabw  3446  cbvrab  3449  ceqsex2  3504  vtocl2gafOLD  3549  vtocl3gaf  3550  spc2ed  3570  rspce  3580  eqvincf  3619  elrabf  3658  elrab3t  3661  rexab2  3673  morex  3693  reu2  3699  rmo3f  3708  reu2eqd  3710  sbc2iegf  3831  reu8nf  3843  rmo2  3853  rmo3  3855  csbiebt  3894  csbie2t  3903  cbvrabcsfw  3906  cbvreucsf  3909  cbvrabcsf  3910  nfdif  4095  nfin  4190  reusngf  4641  rexreusng  4646  reuprg0  4669  rabsnifsb  4689  nfop  4856  nfopd  4857  eluniab  4888  iuneqconst  4970  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  5358  axprlem4OLD  5387  axprlem5OLD  5388  nfpo  5555  nfso  5556  nffr  5614  nfwe  5616  nfxp  5674  opeliunxp  5708  opeliun2xp  5709  nfco  5832  elrnmpt1  5927  nfimad  6043  reuop  6269  iota2  6503  nffun  6542  imadif  6603  nffn  6620  nff  6687  nff1  6757  nffo  6774  nff1o  6801  nffvd  6873  fv3  6879  funimassd  6930  fvmptdf  6977  fompt  7093  f1ossf1o  7103  fmptco  7104  fsnex  7261  nfiso  7300  nfriotadw  7355  cbvriotaw  7356  nfriotad  7358  cbvriota  7360  riota2df  7370  riota5f  7375  oprabv  7452  nfoprab  7456  mpoeq123  7464  nfmpo  7474  cbvoprab1  7479  cbvoprab2  7480  cbvoprab12  7481  cbvoprab3  7483  cbvmpox  7485  ovmpodxf  7542  elovmporab  7638  elovmporab1w  7639  elovmporab1  7640  onminex  7781  fiun  7924  f1iun  7925  opabex3d  7947  opabex3rd  7948  opabex3  7949  dfoprab4f  8038  fmpox  8049  opeliunxp2f  8192  nffrecs  8265  frrlem4  8271  tfr3  8370  tz7.49  8416  naddsuc2  8668  erovlem  8789  nfixpw  8892  nfixp  8893  nfixp1  8894  xpf1o  9109  nneneq  9176  ac6sfi  9238  nfoi  9474  wdom2d  9540  infpssrlem4  10266  hsmexlem2  10387  hsmexlem4  10389  domtriomlem  10402  axdc3lem2  10411  axdc4lem  10415  zorn2lem4  10459  zorn2lem5  10460  konigthlem  10528  axextnd  10551  axrepndlem2  10553  axrepnd  10554  axunnd  10556  axpowndlem2  10558  axpowndlem4  10560  axpownd  10561  axregndlem2  10563  axregnd  10564  axinfndlem1  10565  axinfnd  10566  zfcndrep  10574  zfcndinf  10578  dedekind  11344  dedekindle  11345  fsuppmapnn0fiublem  13962  fsuppmapnn0fiub  13963  fsuppmapnn0fiubex  13964  reuccatpfxs1  14719  nfsum1  15663  nfsum  15664  fsumclf  15711  fsumsplitf  15715  fsumsplit1  15718  fsum2dlem  15743  fsum00  15771  nfcprod1  15881  nfcprod  15882  fprod2dlem  15953  fprodsplitf  15961  fprodsplit1f  15963  fprodle  15969  lcmfunsnlem1  16614  lcmfunsnlem2lem1  16615  lcmfunsnlem2  16617  mreexexd  17616  acsmapd  18520  gsum2d2lem  19910  dprd2d2  19983  gsummoncoe1  22202  gsummatr01lem4  22552  cpmatmcllem  22612  cayleyhamilton1  22786  neiptopnei  23026  neiptopreu  23027  neitr  23074  iunconnlem  23321  iunconn  23322  ptcnplem  23515  ptcnp  23516  xkocnv  23708  isfildlem  23751  utopsnneiplem  24142  isucn2  24173  cfilucfil  24454  restmetu  24465  ovolfiniun  25409  ovoliunlem3  25412  ovoliunnul  25415  volfiniun  25455  itg2splitlem  25656  itg2split  25657  isibl2  25674  nfitg  25683  cbvitg  25684  limciun  25802  2sqmo  27355  2sqreulem4  27372  istrkg2ld  28394  chirred  32331  sbc2iedf  32401  rspc2daf  32402  opreu2reuALT  32413  mo5f  32425  foresf1o  32440  iinabrex  32505  cbvdisjf  32507  disjabrex  32518  disjabrexf  32519  funimass4f  32568  2ndresdju  32580  fmptcof2  32588  fcomptf  32589  acunirnmpt2  32591  acunirnmpt2f  32592  aciunf1lem  32593  funcnv4mpt  32600  fnpreimac  32602  f1od2  32651  fpwrelmap  32663  xrofsup  32697  nn0min  32752  fprodex01  32757  fsumiunle  32761  prodindf  32793  elrgspnsubrunlem2  33206  isarchiofld  33302  nsgqusf1olem1  33391  nsgqusf1olem3  33393  elrspunidl  33406  fedgmullem2  33633  irngnzply1  33693  reff  33836  locfinreflem  33837  cmpcref  33847  zarclsiin  33868  zarcmplem  33878  ordtconnlem1  33921  esumcl  34027  gsumesum  34056  esumlub  34057  esumcst  34060  esumrnmpt2  34065  esumfzf  34066  esumfsup  34067  hasheuni  34082  esumcvg  34083  esumgect  34087  esumcvgre  34088  esum2dlem  34089  esum2d  34090  esumiun  34091  ldsysgenld  34157  sigapildsyslem  34158  sigapildsys  34159  ldgenpisyslem1  34160  measvunilem  34209  measvunilem0  34210  measvuni  34211  measinblem  34217  voliune  34226  volfiniune  34227  volmeas  34228  oms0  34295  omssubadd  34298  eulerpartlemgvv  34374  dstrvprob  34470  breprexplema  34628  bnj919  34764  bnj1146  34788  bnj1379  34827  bnj849  34922  bnj916  34930  bnj964  34940  bnj1014  34958  bnj1123  34983  bnj1228  35008  bnj1307  35020  bnj1321  35024  bnj1398  35031  bnj1408  35033  bnj1444  35040  bnj1445  35041  bnj1446  35042  bnj1449  35045  bnj1467  35051  bnj1463  35052  bnj1489  35053  bnj1491  35054  bnj1312  35055  bnj1525  35066  dvelimalcased  35072  dvelimexcased  35074  fineqvrep  35092  cvmcov  35257  iota5f  35718  axextdist  35794  axextbdist  35795  nfwlim  35817  finminlem  36313  bj-dvelimdv  36846  bj-opabco  37183  isbasisrelowllem1  37350  isbasisrelowllem2  37351  fvineqsneu  37406  fvineqsneq  37407  wl-cbvalnaed  37527  wl-2sb6d  37553  wl-sbalnae  37557  wl-mo2tf  37566  wl-eutf  37568  wl-ax11-lem3  37582  phpreu  37605  poimirlem26  37647  poimirlem27  37648  heicant  37656  mbfposadd  37668  ftc1anclem5  37698  indexdom  37735  filbcmb  37741  sdclem2  37743  sdclem1  37744  fdc1  37747  riotasv2d  38957  riotasv2s  38958  nfded2  38968  glbconxN  39379  pmapglb2xN  39773  cdlemefs32sn1aw  40415  mzpsubmpt  42738  mzpexpmpt  42740  eq0rabdioph  42771  eqrabdioph  42772  setindtr  43020  unielss  43214  nadd1suc  43388  ss2iundf  43655  scottabf  44236  mnuprdlem4  44271  ismnushort  44297  binomcxplemnotnn0  44352  iunconnlem2  44931  nfrelp  44946  modelaxreplem3  44977  modelaxrep  44978  permaxrep  45003  elunif  45017  rspcegf  45024  fnchoice  45030  refsumcn  45031  rfcnnnub  45037  uzwo4  45054  fiiuncl  45066  cbvmpo2  45098  cbvmpo1  45099  iinssiin  45130  disjf1  45184  disjrnmpt2  45189  disjf1o  45192  disjinfi  45193  choicefi  45201  axccdom  45223  dmrelrnrel  45227  axccd  45230  rnmptbddlem  45245  rnmptbd2lem  45249  infnsuprnmpt  45251  rnmptbdlem  45256  rnmptssbi  45261  upbdrech  45310  ssfiunibd  45314  supxrgere  45336  supxrgelem  45340  supxrge  45341  xralrple2  45357  infxr  45370  infxrunb2  45371  xrralrecnnle  45386  xrralrecnnge  45393  supxrunb3  45402  supxrleubrnmpt  45409  infleinf2  45417  unb2ltle  45418  rexabslelem  45421  suprleubrnmpt  45425  uzub  45434  supminfrnmpt  45448  supxrleubrnmptf  45454  infxrgelbrnmpt  45457  infrpgernmpt  45468  monoordxr  45485  monoord2xr  45487  caucvgbf  45492  cvgcaule  45494  iccshift  45523  iooshift  45527  iooiinicc  45547  iooiinioc  45561  fsummulc1f  45576  fsumf1of  45579  fsumreclf  45581  fsumlessf  45582  fmul01  45585  fmuldfeqlem1  45587  fmuldfeq  45588  fmul01lt1lem1  45589  fmul01lt1lem2  45590  fprodexp  45599  mccl  45603  fprodcnlem  45604  fprodcn  45605  climmulf  45609  climexp  45610  climsuse  45613  climrecf  45614  climinff  45616  climaddf  45620  mullimc  45621  islptre  45624  climf  45627  mullimcf  45628  rexlim2d  45630  idlimc  45631  limcperiod  45633  limcrecl  45634  islpcn  45644  limsupre  45646  limcleqr  45649  addlimc  45653  limclner  45656  climsubmpt  45665  climreclf  45669  climf2  45671  climeldmeqmpt  45673  clim2f2  45675  climfveqmpt  45676  fnlimfvre  45679  allbutfifvre  45680  climleltrp  45681  fnlimf  45683  fnlimabslt  45684  climfveqf  45685  climfveqmpt3  45687  climeldmeqf  45688  climeqf  45693  climeldmeqmpt3  45694  limsuppnfd  45707  limsupub  45709  climinf2lem  45711  climinf2  45712  limsuppnf  45716  limsupubuz  45718  climinf2mpt  45719  climinfmpt  45720  climinf3  45721  limsupmnflem  45725  limsupequz  45728  limsupre2  45730  limsupmnfuzlem  45731  limsupequzmptf  45736  limsupre3  45738  limsupre3uzlem  45740  limsupreuzmpt  45744  climisp  45751  lmbr3  45752  climrescn  45753  climxrrelem  45754  climxrre  45755  limsupub2  45817  liminflbuz2  45820  xlimmnfvlem2  45838  xlimmnfv  45839  xlimpnfvlem2  45842  xlimpnfv  45843  xlimmnfmpt  45848  xlimpnfmpt  45849  climxlim2lem  45850  cncficcgt0  45893  cncfioobd  45902  fprodsubrecnncnvlem  45912  fprodaddrecnncnvlem  45914  dvmptmulf  45942  dvnmul  45948  dvmptfprodlem  45949  dvmptfprod  45950  dvnprodlem1  45951  dvnprodlem2  45952  iblsplitf  45975  itgperiod  45986  stoweidlem3  46008  stoweidlem26  46031  stoweidlem27  46032  stoweidlem29  46034  stoweidlem31  46036  stoweidlem34  46039  stoweidlem35  46040  stoweidlem36  46041  stoweidlem39  46044  stoweidlem42  46047  stoweidlem43  46048  stoweidlem44  46049  stoweidlem46  46051  stoweidlem48  46053  stoweidlem49  46054  stoweidlem51  46056  stoweidlem52  46057  stoweidlem53  46058  stoweidlem54  46059  stoweidlem55  46060  stoweidlem56  46061  stoweidlem57  46062  stoweidlem58  46063  stoweidlem59  46064  stoweidlem60  46065  stoweidlem61  46066  stoweidlem62  46067  stoweid  46068  wallispilem3  46072  stirlinglem13  46091  stirling  46094  fourierdlem16  46128  fourierdlem21  46133  fourierdlem22  46134  fourierdlem31  46143  fourierdlem39  46151  fourierdlem48  46159  fourierdlem51  46162  fourierdlem68  46179  fourierdlem71  46182  fourierdlem73  46184  fourierdlem80  46191  fourierdlem81  46192  fourierdlem86  46197  fourierdlem87  46198  fourierdlem93  46204  fourierdlem94  46205  fourierdlem103  46214  fourierdlem104  46215  fourierdlem112  46223  fourierdlem113  46224  elaa2  46239  etransclem32  46271  salexct  46339  sge0revalmpt  46383  sge0f1o  46387  sge0lefi  46403  sge0resplit  46411  sge0lempt  46415  sge0iunmptlemre  46420  sge0fodjrnlem  46421  sge0iunmpt  46423  sge0ltfirpmpt2  46431  sge0isum  46432  sge0xp  46434  sge0isummpt2  46437  sge0xadd  46440  sge0pnffsumgt  46447  sge0gtfsumgt  46448  sge0uzfsumgt  46449  sge0reuz  46452  sge0reuzb  46453  iundjiun  46465  meadjiun  46471  ismeannd  46472  voliunsge0lem  46477  meaiunincf  46488  meaiuninc3v  46489  meaiuninc3  46490  meaiininc  46492  caragenfiiuncl  46520  omeiunltfirp  46524  ovnsubaddlem2  46576  hoidmvval0  46592  hoidmvlelem1  46600  hoidmvlelem3  46602  hoidmvlelem5  46604  ovnlecvr2  46615  hspdifhsp  46621  hoiqssbllem2  46628  hoiqssbllem3  46629  hspmbllem2  46632  opnvonmbllem2  46638  hoimbl2  46670  vonhoire  46677  iinhoiicc  46679  iunhoiioolem  46680  iunhoiioo  46681  vonioo  46687  vonicc  46690  vonn0ioo2  46695  vonn0icc2  46697  salpreimagelt  46712  salpreimalegt  46714  pimincfltioc  46721  pimdecfgtioo  46722  pimincfltioo  46723  preimageiingt  46725  preimaleiinlt  46726  salpreimagtge  46730  salpreimaltle  46731  salpreimalelt  46734  salpreimagtlt  46735  incsmflem  46746  issmflelem  46749  issmfle  46750  smfconst  46754  issmfgtlem  46760  issmfgt  46761  smfaddlem2  46769  smfadd  46770  decsmflem  46771  decsmf  46772  issmfgelem  46774  issmfge  46775  smflimlem2  46777  smflim  46782  smfresal  46793  smfrec  46794  smfmullem4  46799  smfmul  46800  smfpimcc  46813  smflimmpt  46815  smfsuplem1  46816  smfsupmpt  46820  smfsupxr  46821  smfinflem  46822  smfinfmpt  46824  smflimsuplem5  46829  smflimsuplem7  46831  smflimsuplem8  46832  smflimsupmpt  46834  smfliminflem  46835  smfliminfmpt  46837  smfpimne2  46845  fsupdm  46847  smfsupdmmbllem  46849  finfdm  46851  smfinfdmmbllem  46853  or2expropbilem2  47038  or2expropbi  47039  cfsetsnfsetf  47063  2reu8i  47118  nfdfat  47132  iccelpart  47438  ichnfim  47469  ich2exprop  47476  ichreuopeq  47478  sprsymrelfo  47502  reupr  47527  reuopreuprim  47531  2zrngmmgm  48244  cbvmpox2  48328  ovmpordxf  48331  1arymaptfo  48636  2arymaptfo  48647  iinfssclem3  49049  iinfssc  49050  iinfsubc  49051  setrec1  49684  pgindnf  49709  aacllem  49794