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  2301  nfeqf  2386  nfald2  2450  2ax6elem  2475  nfsb4t  2504  nfeu1ALT  2589  eupicka  2634  mopick2  2637  2mo  2648  nfabd2  2923  2ralbida  3269  r19.12  3298  reean  3299  ralcom2  3361  cbvrmow  3393  nfrmow  3397  nfreuw  3398  cbvreuwOLD  3399  cbvreu  3412  cbvrabw  3457  cbvrabwOLD  3458  nfrabw  3459  cbvrab  3463  ceqsex2  3519  vtocl2gafOLD  3564  vtocl3gaf  3565  spc2ed  3585  rspce  3595  eqvincf  3634  elrabf  3672  elrab3t  3675  rexab2  3687  morex  3707  reu2  3713  rmo3f  3722  reu2eqd  3724  sbc2iegf  3845  reu8nf  3857  rmo2  3867  rmo3  3869  csbiebt  3908  csbie2t  3917  cbvrabcsfw  3920  cbvreucsf  3923  cbvrabcsf  3924  nfdif  4109  nfin  4204  reusngf  4655  rexreusng  4660  reuprg0  4683  rabsnifsb  4703  nfop  4870  nfopd  4871  eluniab  4902  iuneqconst  4984  cbvopab  5196  cbvopab1  5198  cbvopab1g  5199  cbvopab2  5200  cbvopab1s  5201  mpteq12f  5210  nfmpt  5224  cbvmptf  5226  cbvmptfg  5227  axrep3  5258  axrep4OLD  5261  axrep5  5262  reusv2lem3  5375  axprlem4OLD  5404  axprlem5OLD  5405  nfpo  5572  nfso  5573  nffr  5632  nfwe  5634  nfxp  5692  opeliunxp  5726  opeliun2xp  5727  nfco  5850  elrnmpt1  5945  nfimad  6061  reuop  6287  iota2  6525  nffun  6564  imadif  6625  nffn  6642  nff  6707  nff1  6777  nffo  6794  nff1o  6821  nffvd  6893  fv3  6899  funimassd  6950  fvmptdf  6997  fompt  7113  f1ossf1o  7123  fmptco  7124  fsnex  7281  nfiso  7320  nfriotadw  7375  cbvriotaw  7376  nfriotad  7378  cbvriota  7380  riota2df  7390  riota5f  7395  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  7801  fiun  7946  f1iun  7947  opabex3d  7969  opabex3rd  7970  opabex3  7971  dfoprab4f  8060  fmpox  8071  opeliunxp2f  8214  nffrecs  8287  frrlem4  8293  nfwrecsOLD  8321  wfrlem4OLD  8331  tfr3  8418  tz7.49  8464  naddsuc2  8718  erovlem  8832  nfixpw  8935  nfixp  8936  nfixp1  8937  xpf1o  9158  nneneq  9225  ac6sfi  9297  nfoi  9533  wdom2d  9599  infpssrlem4  10325  hsmexlem2  10446  hsmexlem4  10448  domtriomlem  10461  axdc3lem2  10470  axdc4lem  10474  zorn2lem4  10518  zorn2lem5  10519  konigthlem  10587  axextnd  10610  axrepndlem2  10612  axrepnd  10613  axunnd  10615  axpowndlem2  10617  axpowndlem4  10619  axpownd  10620  axregndlem2  10622  axregnd  10623  axinfndlem1  10624  axinfnd  10625  zfcndrep  10633  zfcndinf  10637  dedekind  11403  dedekindle  11404  fsuppmapnn0fiublem  14013  fsuppmapnn0fiub  14014  fsuppmapnn0fiubex  14015  reuccatpfxs1  14770  nfsum1  15711  nfsum  15712  fsumclf  15759  fsumsplitf  15763  fsumsplit1  15766  fsum2dlem  15791  fsum00  15819  nfcprod1  15929  nfcprod  15930  fprod2dlem  16001  fprodsplitf  16009  fprodsplit1f  16011  fprodle  16017  lcmfunsnlem1  16661  lcmfunsnlem2lem1  16662  lcmfunsnlem2  16664  mreexexd  17665  acsmapd  18569  gsum2d2lem  19959  dprd2d2  20032  gsummoncoe1  22251  gsummatr01lem4  22601  cpmatmcllem  22661  cayleyhamilton1  22835  neiptopnei  23075  neiptopreu  23076  neitr  23123  iunconnlem  23370  iunconn  23371  ptcnplem  23564  ptcnp  23565  xkocnv  23757  isfildlem  23800  utopsnneiplem  24191  isucn2  24222  cfilucfil  24503  restmetu  24514  ovolfiniun  25459  ovoliunlem3  25462  ovoliunnul  25465  volfiniun  25505  itg2splitlem  25706  itg2split  25707  isibl2  25724  nfitg  25733  cbvitg  25734  limciun  25852  2sqmo  27405  2sqreulem4  27422  istrkg2ld  28444  chirred  32381  sbc2iedf  32451  rspc2daf  32452  opreu2reuALT  32463  mo5f  32475  foresf1o  32490  iinabrex  32555  cbvdisjf  32557  disjabrex  32568  disjabrexf  32569  funimass4f  32620  2ndresdju  32632  fmptcof2  32640  fcomptf  32641  acunirnmpt2  32643  acunirnmpt2f  32644  aciunf1lem  32645  funcnv4mpt  32652  fnpreimac  32654  f1od2  32703  fpwrelmap  32715  xrofsup  32749  nn0min  32804  fprodex01  32809  fsumiunle  32813  prodindf  32845  elrgspnsubrunlem2  33248  isarchiofld  33344  nsgqusf1olem1  33433  nsgqusf1olem3  33435  elrspunidl  33448  fedgmullem2  33675  irngnzply1  33737  reff  33875  locfinreflem  33876  cmpcref  33886  zarclsiin  33907  zarcmplem  33917  ordtconnlem1  33960  esumcl  34066  gsumesum  34095  esumlub  34096  esumcst  34099  esumrnmpt2  34104  esumfzf  34105  esumfsup  34106  hasheuni  34121  esumcvg  34122  esumgect  34126  esumcvgre  34127  esum2dlem  34128  esum2d  34129  esumiun  34130  ldsysgenld  34196  sigapildsyslem  34197  sigapildsys  34198  ldgenpisyslem1  34199  measvunilem  34248  measvunilem0  34249  measvuni  34250  measinblem  34256  voliune  34265  volfiniune  34266  volmeas  34267  oms0  34334  omssubadd  34337  eulerpartlemgvv  34413  dstrvprob  34509  breprexplema  34667  bnj919  34803  bnj1146  34827  bnj1379  34866  bnj849  34961  bnj916  34969  bnj964  34979  bnj1014  34997  bnj1123  35022  bnj1228  35047  bnj1307  35059  bnj1321  35063  bnj1398  35070  bnj1408  35072  bnj1444  35079  bnj1445  35080  bnj1446  35081  bnj1449  35084  bnj1467  35090  bnj1463  35091  bnj1489  35092  bnj1491  35093  bnj1312  35094  bnj1525  35105  dvelimalcased  35111  dvelimexcased  35113  fineqvrep  35131  cvmcov  35290  iota5f  35746  axextdist  35822  axextbdist  35823  nfwlim  35845  finminlem  36341  bj-dvelimdv  36874  bj-opabco  37211  isbasisrelowllem1  37378  isbasisrelowllem2  37379  fvineqsneu  37434  fvineqsneq  37435  wl-cbvalnaed  37555  wl-2sb6d  37581  wl-sbalnae  37585  wl-mo2tf  37594  wl-eutf  37596  wl-ax11-lem3  37610  phpreu  37633  poimirlem26  37675  poimirlem27  37676  heicant  37684  mbfposadd  37696  ftc1anclem5  37726  indexdom  37763  filbcmb  37769  sdclem2  37771  sdclem1  37772  fdc1  37775  riotasv2d  38980  riotasv2s  38981  nfded2  38991  glbconxN  39402  pmapglb2xN  39796  cdlemefs32sn1aw  40438  mzpsubmpt  42741  mzpexpmpt  42743  eq0rabdioph  42774  eqrabdioph  42775  setindtr  43023  unielss  43217  nadd1suc  43391  ss2iundf  43658  scottabf  44239  mnuprdlem4  44274  ismnushort  44300  binomcxplemnotnn0  44355  iunconnlem2  44934  nfrelp  44949  modelaxreplem3  44980  modelaxrep  44981  permaxrep  45006  elunif  45020  rspcegf  45027  fnchoice  45033  refsumcn  45034  rfcnnnub  45040  uzwo4  45057  fiiuncl  45069  cbvmpo2  45101  cbvmpo1  45102  iinssiin  45133  disjf1  45187  disjrnmpt2  45192  disjf1o  45195  disjinfi  45196  choicefi  45204  axccdom  45226  dmrelrnrel  45230  axccd  45233  rnmptbddlem  45248  rnmptbd2lem  45252  infnsuprnmpt  45254  rnmptbdlem  45259  rnmptssbi  45264  upbdrech  45314  ssfiunibd  45318  supxrgere  45340  supxrgelem  45344  supxrge  45345  xralrple2  45361  infxr  45374  infxrunb2  45375  xrralrecnnle  45390  xrralrecnnge  45397  supxrunb3  45406  supxrleubrnmpt  45413  infleinf2  45421  unb2ltle  45422  rexabslelem  45425  suprleubrnmpt  45429  uzub  45438  supminfrnmpt  45452  supxrleubrnmptf  45458  infxrgelbrnmpt  45461  infrpgernmpt  45472  monoordxr  45489  monoord2xr  45491  caucvgbf  45496  cvgcaule  45498  iccshift  45527  iooshift  45531  iooiinicc  45551  iooiinioc  45565  fsummulc1f  45580  fsumf1of  45583  fsumreclf  45585  fsumlessf  45586  fmul01  45589  fmuldfeqlem1  45591  fmuldfeq  45592  fmul01lt1lem1  45593  fmul01lt1lem2  45594  fprodexp  45603  mccl  45607  fprodcnlem  45608  fprodcn  45609  climmulf  45613  climexp  45614  climsuse  45617  climrecf  45618  climinff  45620  climaddf  45624  mullimc  45625  islptre  45628  climf  45631  mullimcf  45632  rexlim2d  45634  idlimc  45635  limcperiod  45637  limcrecl  45638  islpcn  45648  limsupre  45650  limcleqr  45653  addlimc  45657  limclner  45660  climsubmpt  45669  climreclf  45673  climf2  45675  climeldmeqmpt  45677  clim2f2  45679  climfveqmpt  45680  fnlimfvre  45683  allbutfifvre  45684  climleltrp  45685  fnlimf  45687  fnlimabslt  45688  climfveqf  45689  climfveqmpt3  45691  climeldmeqf  45692  climeqf  45697  climeldmeqmpt3  45698  limsuppnfd  45711  limsupub  45713  climinf2lem  45715  climinf2  45716  limsuppnf  45720  limsupubuz  45722  climinf2mpt  45723  climinfmpt  45724  climinf3  45725  limsupmnflem  45729  limsupequz  45732  limsupre2  45734  limsupmnfuzlem  45735  limsupequzmptf  45740  limsupre3  45742  limsupre3uzlem  45744  limsupreuzmpt  45748  climisp  45755  lmbr3  45756  climrescn  45757  climxrrelem  45758  climxrre  45759  limsupub2  45821  liminflbuz2  45824  xlimmnfvlem2  45842  xlimmnfv  45843  xlimpnfvlem2  45846  xlimpnfv  45847  xlimmnfmpt  45852  xlimpnfmpt  45853  climxlim2lem  45854  cncficcgt0  45897  cncfioobd  45906  fprodsubrecnncnvlem  45916  fprodaddrecnncnvlem  45918  dvmptmulf  45946  dvnmul  45952  dvmptfprodlem  45953  dvmptfprod  45954  dvnprodlem1  45955  dvnprodlem2  45956  iblsplitf  45979  itgperiod  45990  stoweidlem3  46012  stoweidlem26  46035  stoweidlem27  46036  stoweidlem29  46038  stoweidlem31  46040  stoweidlem34  46043  stoweidlem35  46044  stoweidlem36  46045  stoweidlem39  46048  stoweidlem42  46051  stoweidlem43  46052  stoweidlem44  46053  stoweidlem46  46055  stoweidlem48  46057  stoweidlem49  46058  stoweidlem51  46060  stoweidlem52  46061  stoweidlem53  46062  stoweidlem54  46063  stoweidlem55  46064  stoweidlem56  46065  stoweidlem57  46066  stoweidlem58  46067  stoweidlem59  46068  stoweidlem60  46069  stoweidlem61  46070  stoweidlem62  46071  stoweid  46072  wallispilem3  46076  stirlinglem13  46095  stirling  46098  fourierdlem16  46132  fourierdlem21  46137  fourierdlem22  46138  fourierdlem31  46147  fourierdlem39  46155  fourierdlem48  46163  fourierdlem51  46166  fourierdlem68  46183  fourierdlem71  46186  fourierdlem73  46188  fourierdlem80  46195  fourierdlem81  46196  fourierdlem86  46201  fourierdlem87  46202  fourierdlem93  46208  fourierdlem94  46209  fourierdlem103  46218  fourierdlem104  46219  fourierdlem112  46227  fourierdlem113  46228  elaa2  46243  etransclem32  46275  salexct  46343  sge0revalmpt  46387  sge0f1o  46391  sge0lefi  46407  sge0resplit  46415  sge0lempt  46419  sge0iunmptlemre  46424  sge0fodjrnlem  46425  sge0iunmpt  46427  sge0ltfirpmpt2  46435  sge0isum  46436  sge0xp  46438  sge0isummpt2  46441  sge0xadd  46444  sge0pnffsumgt  46451  sge0gtfsumgt  46452  sge0uzfsumgt  46453  sge0reuz  46456  sge0reuzb  46457  iundjiun  46469  meadjiun  46475  ismeannd  46476  voliunsge0lem  46481  meaiunincf  46492  meaiuninc3v  46493  meaiuninc3  46494  meaiininc  46496  caragenfiiuncl  46524  omeiunltfirp  46528  ovnsubaddlem2  46580  hoidmvval0  46596  hoidmvlelem1  46604  hoidmvlelem3  46606  hoidmvlelem5  46608  ovnlecvr2  46619  hspdifhsp  46625  hoiqssbllem2  46632  hoiqssbllem3  46633  hspmbllem2  46636  opnvonmbllem2  46642  hoimbl2  46674  vonhoire  46681  iinhoiicc  46683  iunhoiioolem  46684  iunhoiioo  46685  vonioo  46691  vonicc  46694  vonn0ioo2  46699  vonn0icc2  46701  salpreimagelt  46716  salpreimalegt  46718  pimincfltioc  46725  pimdecfgtioo  46726  pimincfltioo  46727  preimageiingt  46729  preimaleiinlt  46730  salpreimagtge  46734  salpreimaltle  46735  salpreimalelt  46738  salpreimagtlt  46739  incsmflem  46750  issmflelem  46753  issmfle  46754  smfconst  46758  issmfgtlem  46764  issmfgt  46765  smfaddlem2  46773  smfadd  46774  decsmflem  46775  decsmf  46776  issmfgelem  46778  issmfge  46779  smflimlem2  46781  smflim  46786  smfresal  46797  smfrec  46798  smfmullem4  46803  smfmul  46804  smfpimcc  46817  smflimmpt  46819  smfsuplem1  46820  smfsupmpt  46824  smfsupxr  46825  smfinflem  46826  smfinfmpt  46828  smflimsuplem5  46833  smflimsuplem7  46835  smflimsuplem8  46836  smflimsupmpt  46838  smfliminflem  46839  smfliminfmpt  46841  smfpimne2  46849  fsupdm  46851  smfsupdmmbllem  46853  finfdm  46855  smfinfdmmbllem  46857  or2expropbilem2  47042  or2expropbi  47043  cfsetsnfsetf  47067  2reu8i  47122  nfdfat  47136  iccelpart  47427  ichnfim  47458  ich2exprop  47465  ichreuopeq  47467  sprsymrelfo  47491  reupr  47516  reuopreuprim  47520  2zrngmmgm  48207  cbvmpox2  48291  ovmpordxf  48294  1arymaptfo  48603  2arymaptfo  48614  iinfssclem3  49003  iinfssc  49004  iinfsubc  49005  setrec1  49535  pgindnf  49560  aacllem  49645