Theorem nfan 1932

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

This proof depends on syntax axioms:   ∧ wa 401  ⊤wtru 1571  Ⅎwnf 1816

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

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817

This theorem is used by:  nfnan  1933  nf3an  1934  hban  2335  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  3364  cbvrmow  3392  nfrmow  3396  nfreuw  3397  cbvreu  3406  cbvrabw  3449  nfrabw  3450  cbvrab  3452  ceqsex2  3503  vtocl3gaf  3542  spc2ed  3558  rspce  3568  eqvincf  3607  elrabf  3645  elrab3t  3647  rexab2  3660  morex  3680  reu2  3686  rmo3f  3695  reu2eqd  3697  sbc2iegf  3816  reu8nf  3827  rmo2  3837  rmo3  3839  csbiebt  3879  csbie2t  3888  cbvrabcsfw  3891  cbvreucsf  3894  cbvrabcsf  3895  nfdif  4080  nfin  4173  reusngf  4638  rexreusng  4643  reuprg0  4666  rabsnifsb  4686  nfop  4852  nfopd  4853  eluniab  4884  iuneqconst  4966  cbvopab  5181  cbvopab1  5183  cbvopab1g  5184  cbvopab2  5185  cbvopab1s  5186  mpteq12f  5194  nfmpt  5207  cbvmptf  5209  cbvmptfg  5210  axrep3  5240  axrep4OLD  5243  axrep5  5244  reusv2lem3  5369  axprlem4OLD  5399  axprlem5OLD  5400  nfpo  5573  nfso  5574  nffr  5632  nfwe  5634  nfxp  5692  opeliunxp  5726  opeliun2xp  5727  nfco  5849  elrnmpt1  5948  nfimad  6069  reuop  6295  iota2  6526  nffun  6560  imadif  6621  nffn  6635  nff  6702  nff1  6773  nffo  6792  nff1o  6819  nffvd  6894  fv3  6900  funimassd  6948  fvmptdf  6997  fompt  7114  f1ossf1o  7125  fmptco  7126  fsnex  7287  nfiso  7326  nfriotadw  7381  cbvriotaw  7382  nfriotad  7384  cbvriota  7386  riota2df  7396  riota5f  7401  oprabv  7476  nfoprab  7480  mpoeq123  7488  nfmpo  7498  cbvoprab1  7503  cbvoprab2  7504  cbvoprab12  7505  cbvoprab3  7507  cbvmpox  7509  ovmpodxf  7566  elovmporab  7663  elovmporab1w  7664  elovmporab1  7665  onminex  7804  fiun  7943  f1iun  7944  opabex3d  7965  opabex3rd  7966  opabex3  7967  dfoprab4f  8056  fmpox  8067  opeliunxp2f  8211  nffrecs  8285  frrlem4  8291  tfr3  8391  tz7.49  8437  naddsuc2  8693  erovlem  8816  nfixpw  8926  nfixp  8927  nfixp1  8928  xpf1o  9140  nneneq  9203  ac6sfi  9257  nfoi  9489  wdom2d  9555  scottabf  9881  infpssrlem4  10311  hsmexlem2  10432  hsmexlem4  10434  domtriomlem  10447  axdc3lem2  10456  axdc4lem  10460  zorn2lem4  10504  zorn2lem5  10505  konigthlem  10580  axextnd  10603  axrepndlem2  10605  axrepnd  10606  axunnd  10608  axpowndlem2  10610  axpowndlem4  10612  axpownd  10613  axregndlem2  10615  axregnd  10616  axinfndlem1  10617  axinfnd  10618  zfcndrep  10626  zfcndinf  10630  dedekind  11400  dedekindle  11401  fsuppmapnn0fiublem  14056  fsuppmapnn0fiub  14057  fsuppmapnn0fiubex  14058  reuccatpfxs1  14818  nfsum1  15779  nfsum  15780  fsumclf  15826  fsumsplitf  15830  fsumsplit1  15833  fsum2dlem  15858  fsum00  15887  nfcprod1  15999  nfcprod  16000  fprod2dlem  16071  fprodsplitf  16079  fprodsplit1f  16081  fprodle  16087  lcmfunsnlem1  16731  lcmfunsnlem2lem1  16732  lcmfunsnlem2  16734  mreexexd  17740  acsmapd  18646  gsum2d2lem  20104  dprd2d2  20177  gsummoncoe1  22537  gsummatr01lem4  22884  cpmatmcllem  22947  cayleyhamilton1  23121  neiptopnei  23361  neiptopreu  23362  neitr  23409  iunconnlem  23656  iunconn  23657  ptcnplem  23851  ptcnp  23852  xkocnv  24044  isfildlem  24087  utopsnneiplem  24477  isucn2  24508  cfilucfil  24789  restmetu  24800  ovolfiniun  25733  ovoliunlem3  25736  ovoliunnul  25739  volfiniun  25779  itg2splitlem  25980  itg2split  25981  isibl2  25998  nfitg  26007  cbvitg  26008  limciun  26126  2sqmo  27674  2sqreulem4  27691  bdaypw2n0bndlem  28729  istrkg2ld  28802  chirred  32877  sbc2iedf  32942  rspc2daf  32943  opreu2reuALT  32953  mo5f  32965  foresf1o  32980  iinabrex  33044  cbvdisjf  33046  disjabrex  33057  disjabrexf  33058  funimass4f  33112  2ndresdju  33124  fmptcof2  33132  fcomptf  33133  acunirnmpt2  33135  acunirnmpt2f  33136  aciunf1lem  33137  funcnv4mpt  33143  fnpreimac  33145  f1od2  33192  fpwrelmap  33206  xrofsup  33240  nn0min  33293  fprodex01  33297  fsumiunle  33301  prodindf  33310  suppgsumssiun  33514  isarchiofld  33641  elrgspnsubrunlem2  33690  nsgqusf1olem1  33844  nsgqusf1olem3  33846  elrspunidl  33858  deg1prod  33995  mplvrpmga  34057  esplyfval1  34085  vieta  34092  fedgmullem2  34142  irngnzply1  34203  reff  34351  locfinreflem  34352  cmpcref  34362  zarclsiin  34383  zarcmplem  34393  ordtconnlem1  34436  esumcl  34542  gsumesum  34571  esumlub  34572  esumcst  34575  esumrnmpt2  34580  esumfzf  34581  esumfsup  34582  hasheuni  34597  esumcvg  34598  esumgect  34602  esumcvgre  34603  esum2dlem  34604  esum2d  34605  esumiun  34606  ldsysgenld  34673  sigapildsyslem  34674  sigapildsys  34675  ldgenpisyslem1  34676  measvunilem  34725  measvunilem0  34726  measvuni  34727  measinblem  34733  voliune  34742  volfiniune  34743  volmeas  34744  oms0  34810  omssubadd  34813  eulerpartlemgvv  34889  dstrvprob  34985  breprexplema  35140  bnj919  35279  bnj1146  35302  bnj1379  35341  bnj849  35436  bnj916  35444  bnj964  35454  bnj1014  35472  bnj1123  35497  bnj1228  35522  bnj1307  35534  bnj1321  35538  bnj1398  35545  bnj1408  35547  bnj1444  35554  bnj1445  35555  bnj1446  35556  bnj1449  35559  bnj1467  35565  bnj1463  35566  bnj1489  35567  bnj1491  35568  bnj1312  35569  bnj1525  35580  dvelimalcased  35586  dvelimexcased  35588  fineqvrep  35642  cvmcov  35844  iota5f  36305  axextdist  36378  axextbdist  36379  nfwlim  36401  finminlem  36939  axtcond  37099  bj-dvelimdv  37596  bj-axreprepsep  37822  bj-opabco  37942  isbasisrelowllem1  38111  isbasisrelowllem2  38112  fvineqsneu  38167  fvineqsneq  38168  wl-cbvalnaed  38297  wl-2sb6d  38323  wl-sbalnae  38327  wl-mo2tf  38336  wl-eutf  38338  phpreu  38360  poimirlem26  38397  poimirlem27  38398  heicant  38406  mbfposadd  38418  ftc1anclem5  38448  indexdom  38486  filbcmb  38492  sdclem2  38494  sdclem1  38495  fdc1  38498  riotasv2d  39832  riotasv2s  39833  nfded2  39843  glbconxN  40253  pmapglb2xN  40647  cdlemefs32sn1aw  41289  mzpsubmpt  43590  mzpexpmpt  43592  eq0rabdioph  43623  eqrabdioph  43624  setindtr  43867  unielss  44061  nadd1suc  44235  ss2iundf  44501  mnuprdlem4  45101  ismnushort  45127  binomcxplemnotnn0  45182  iunconnlem2  45759  nfrelp  45774  modelaxreplem3  45805  modelaxrep  45806  permaxrep  45831  elunif  45852  rspcegf  45859  fnchoice  45865  refsumcn  45866  rfcnnnub  45872  uzwo4  45889  fiiuncl  45901  cbvmpo2  45931  cbvmpo1  45932  iinssiin  45963  disjf1  46017  disjrnmpt2  46022  disjf1o  46025  disjinfi  46026  choicefi  46033  axccdom  46054  dmrelrnrel  46058  axccd  46060  rnmptbddlem  46075  rnmptbd2lem  46079  infnsuprnmpt  46081  rnmptbdlem  46086  rnmptssbi  46091  upbdrech  46140  ssfiunibd  46144  supxrgere  46165  supxrgelem  46169  supxrge  46170  xralrple2  46186  infxr  46198  infxrunb2  46199  xrralrecnnle  46214  xrralrecnnge  46221  supxrunb3  46230  supxrleubrnmpt  46236  infleinf2  46244  unb2ltle  46245  rexabslelem  46248  suprleubrnmpt  46252  uzub  46261  supminfrnmpt  46275  supxrleubrnmptf  46281  infxrgelbrnmpt  46284  infrpgernmpt  46295  monoordxr  46312  monoord2xr  46314  caucvgbf  46319  cvgcaule  46321  iccshift  46350  iooshift  46354  iooiinicc  46374  iooiinioc  46388  fsummulc1f  46403  fsumf1of  46406  fsumreclf  46408  fsumlessf  46409  fmul01  46412  fmuldfeqlem1  46414  fmuldfeq  46415  fmul01lt1lem1  46416  fmul01lt1lem2  46417  fprodexp  46426  mccl  46430  fprodcnlem  46431  fprodcn  46432  climmulf  46436  climexp  46437  climsuse  46440  climrecf  46441  climinff  46443  climaddf  46447  mullimc  46448  islptre  46451  climf  46454  mullimcf  46455  rexlim2d  46457  idlimc  46458  limcperiod  46460  limcrecl  46461  islpcn  46469  limsupre  46471  limcleqr  46474  addlimc  46478  limclner  46481  climsubmpt  46490  climreclf  46494  climf2  46496  climeldmeqmpt  46498  clim2f2  46500  climfveqmpt  46501  fnlimfvre  46504  allbutfifvre  46505  climleltrp  46506  fnlimf  46508  fnlimabslt  46509  climfveqf  46510  climfveqmpt3  46512  climeldmeqf  46513  climeqf  46518  climeldmeqmpt3  46519  limsuppnfd  46532  limsupub  46534  climinf2lem  46536  climinf2  46537  limsuppnf  46541  limsupubuz  46543  climinf2mpt  46544  climinfmpt  46545  climinf3  46546  limsupmnflem  46550  limsupequz  46553  limsupre2  46555  limsupmnfuzlem  46556  limsupequzmptf  46561  limsupre3  46563  limsupre3uzlem  46565  limsupreuzmpt  46569  climisp  46576  lmbr3  46577  climrescn  46578  climxrrelem  46579  climxrre  46580  limsupub2  46642  liminflbuz2  46645  xlimmnfvlem2  46663  xlimmnfv  46664  xlimpnfvlem2  46667  xlimpnfv  46668  xlimmnfmpt  46673  xlimpnfmpt  46674  climxlim2lem  46675  cncficcgt0  46718  cncfioobd  46727  fprodsubrecnncnvlem  46737  fprodaddrecnncnvlem  46739  dvmptmulf  46767  dvnmul  46773  dvmptfprodlem  46774  dvmptfprod  46775  dvnprodlem1  46776  dvnprodlem2  46777  iblsplitf  46800  itgperiod  46811  stoweidlem3  46833  stoweidlem26  46856  stoweidlem27  46857  stoweidlem29  46859  stoweidlem31  46861  stoweidlem34  46864  stoweidlem35  46865  stoweidlem36  46866  stoweidlem39  46869  stoweidlem42  46872  stoweidlem43  46873  stoweidlem44  46874  stoweidlem46  46876  stoweidlem48  46878  stoweidlem49  46879  stoweidlem51  46881  stoweidlem52  46882  stoweidlem53  46883  stoweidlem54  46884  stoweidlem55  46885  stoweidlem56  46886  stoweidlem57  46887  stoweidlem58  46888  stoweidlem59  46889  stoweidlem60  46890  stoweidlem61  46891  stoweidlem62  46892  stoweid  46893  wallispilem3  46897  stirlinglem13  46916  stirling  46919  fourierdlem16  46953  fourierdlem21  46958  fourierdlem22  46959  fourierdlem31  46968  fourierdlem39  46976  fourierdlem48  46984  fourierdlem51  46987  fourierdlem68  47004  fourierdlem71  47007  fourierdlem73  47009  fourierdlem80  47016  fourierdlem81  47017  fourierdlem86  47022  fourierdlem87  47023  fourierdlem93  47029  fourierdlem94  47030  fourierdlem103  47039  fourierdlem104  47040  fourierdlem112  47048  fourierdlem113  47049  elaa2  47064  etransclem32  47096  salexct  47164  sge0revalmpt  47208  sge0f1o  47212  sge0lefi  47228  sge0resplit  47236  sge0lempt  47240  sge0iunmptlemre  47245  sge0fodjrnlem  47246  sge0iunmpt  47248  sge0ltfirpmpt2  47256  sge0isum  47257  sge0xp  47259  sge0isummpt2  47262  sge0xadd  47265  sge0pnffsumgt  47272  sge0gtfsumgt  47273  sge0uzfsumgt  47274  sge0reuz  47277  sge0reuzb  47278  iundjiun  47290  meadjiun  47296  ismeannd  47297  voliunsge0lem  47302  meaiunincf  47313  meaiuninc3v  47314  meaiuninc3  47315  meaiininc  47317  caragenfiiuncl  47345  omeiunltfirp  47349  ovnsubaddlem2  47401  hoidmvval0  47417  hoidmvlelem1  47425  hoidmvlelem3  47427  hoidmvlelem5  47429  ovnlecvr2  47440  hspdifhsp  47446  hoiqssbllem2  47453  hoiqssbllem3  47454  hspmbllem2  47457  opnvonmbllem2  47463  hoimbl2  47495  vonhoire  47502  iinhoiicc  47504  iunhoiioolem  47505  iunhoiioo  47506  vonioo  47512  vonicc  47515  vonn0ioo2  47520  vonn0icc2  47522  salpreimagelt  47537  salpreimalegt  47539  pimincfltioc  47546  pimdecfgtioo  47547  pimincfltioo  47548  preimageiingt  47550  preimaleiinlt  47551  salpreimagtge  47555  salpreimaltle  47556  salpreimalelt  47559  salpreimagtlt  47560  incsmflem  47571  issmflelem  47574  issmfle  47575  smfconst  47579  issmfgtlem  47585  issmfgt  47586  smfaddlem2  47594  smfadd  47595  decsmflem  47596  decsmf  47597  issmfgelem  47599  issmfge  47600  smflimlem2  47602  smflim  47607  smfresal  47618  smfrec  47619  smfmullem4  47624  smfmul  47625  smfpimcc  47638  smflimmpt  47640  smfsuplem1  47641  smfsupmpt  47645  smfsupxr  47646  smfinflem  47647  smfinfmpt  47649  smflimsuplem5  47654  smflimsuplem7  47656  smflimsuplem8  47657  smflimsupmpt  47659  smfliminflem  47660  smfliminfmpt  47662  smfpimne2  47670  fsupdm  47672  smfsupdmmbllem  47674  finfdm  47676  smfinfdmmbllem  47678  or2expropbilem2  47923  or2expropbi  47924  cfsetsnfsetf  47948  2reu8i  48003  nfdfat  48017  iccelpart  48335  ichnfim  48366  ich2exprop  48373  ichreuopeq  48375  sprsymrelfo  48399  reupr  48424  reuopreuprim  48428  2zrngmmgm  49169  cbvmpox2  49268  ovmpordxf  49271  1arymaptfo  49575  2arymaptfo  49586  iinfssclem3  49984  iinfssc  49985  iinfsubc  49986  setrec1  50619  pgindnf  50644  nfals  50734  nfrals  50735  nfalseu  50765  nfralseu  50766  aacllem  50774