Theorem nfan 1927

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

Syntax hints:   ∧ wa 400  ⊤wtru 1569  Ⅎwnf 1811

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1571  df-ex 1808  df-nf 1812

This theorem is referenced by:  nfnan  1928  nf3an  1929  hban  2333  nfeqf  2411  nfald2  2475  2ax6elem  2500  nfsb4t  2529  nfeu1  2615  eupicka  2660  mopick2  2663  2mo  2674  nfabd2  2946  2ralbida  3286  r19.12  3312  reean  3313  ralcom2  3364  cbvrmow  3392  nfrmow  3396  nfreuw  3397  cbvreu  3406  cbvrabw  3449  nfrabw  3450  cbvrab  3452  ceqsex2  3503  vtocl3gaf  3543  spc2ed  3559  rspce  3569  eqvincf  3608  elrabf  3646  elrab3t  3648  rexab2  3661  morex  3681  reu2  3687  rmo3f  3696  reu2eqd  3698  sbc2iegf  3817  reu8nf  3829  rmo2  3839  rmo3  3841  csbiebt  3881  csbie2t  3890  cbvrabcsfw  3893  cbvreucsf  3896  cbvrabcsf  3897  nfdif  4083  nfin  4176  reusngf  4639  rexreusng  4644  reuprg0  4667  rabsnifsb  4687  nfop  4853  nfopd  4854  eluniab  4885  iuneqconst  4967  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  5371  axprlem4OLD  5401  axprlem5OLD  5402  nfpo  5575  nfso  5576  nffr  5634  nfwe  5636  nfxp  5694  opeliunxp  5728  opeliun2xp  5729  nfco  5851  elrnmpt1  5950  nfimad  6071  reuop  6294  iota2  6525  nffun  6559  imadif  6620  nffn  6634  nff  6701  nff1  6772  nffo  6791  nff1o  6818  nffvd  6893  fv3  6899  funimassd  6947  fvmptdf  6996  fompt  7113  f1ossf1o  7124  fmptco  7125  fsnex  7281  nfiso  7320  nfriotadw  7375  cbvriotaw  7376  nfriotad  7378  cbvriota  7380  riota2df  7390  riota5f  7395  oprabv  7470  nfoprab  7474  mpoeq123  7482  nfmpo  7492  cbvoprab1  7497  cbvoprab2  7498  cbvoprab12  7499  cbvoprab3  7501  cbvmpox  7503  ovmpodxf  7560  elovmporab  7656  elovmporab1w  7657  elovmporab1  7658  onminex  7800  fiun  7939  f1iun  7940  opabex3d  7961  opabex3rd  7962  opabex3  7963  dfoprab4f  8052  fmpox  8063  opeliunxp2f  8205  nffrecs  8279  frrlem4  8285  tfr3  8385  tz7.49  8431  naddsuc2  8687  erovlem  8810  nfixpw  8913  nfixp  8914  nfixp1  8915  xpf1o  9126  nneneq  9189  ac6sfi  9243  nfoi  9475  wdom2d  9541  scottabf  9865  infpssrlem4  10289  hsmexlem2  10410  hsmexlem4  10412  domtriomlem  10425  axdc3lem2  10434  axdc4lem  10438  zorn2lem4  10482  zorn2lem5  10483  konigthlem  10552  axextnd  10575  axrepndlem2  10577  axrepnd  10578  axunnd  10580  axpowndlem2  10582  axpowndlem4  10584  axpownd  10585  axregndlem2  10587  axregnd  10588  axinfndlem1  10589  axinfnd  10590  zfcndrep  10598  zfcndinf  10602  dedekind  11372  dedekindle  11373  fsuppmapnn0fiublem  14026  fsuppmapnn0fiub  14027  fsuppmapnn0fiubex  14028  reuccatpfxs1  14784  nfsum1  15741  nfsum  15742  fsumclf  15789  fsumsplitf  15793  fsumsplit1  15796  fsum2dlem  15821  fsum00  15850  nfcprod1  15962  nfcprod  15963  fprod2dlem  16034  fprodsplitf  16042  fprodsplit1f  16044  fprodle  16050  lcmfunsnlem1  16694  lcmfunsnlem2lem1  16695  lcmfunsnlem2  16697  mreexexd  17703  acsmapd  18609  gsum2d2lem  20042  dprd2d2  20115  gsummoncoe1  22447  gsummatr01lem4  22794  cpmatmcllem  22854  cayleyhamilton1  23028  neiptopnei  23268  neiptopreu  23269  neitr  23316  iunconnlem  23563  iunconn  23564  ptcnplem  23757  ptcnp  23758  xkocnv  23950  isfildlem  23993  utopsnneiplem  24383  isucn2  24414  cfilucfil  24695  restmetu  24706  ovolfiniun  25639  ovoliunlem3  25642  ovoliunnul  25645  volfiniun  25685  itg2splitlem  25886  itg2split  25887  isibl2  25904  nfitg  25913  cbvitg  25914  limciun  26032  2sqmo  27577  2sqreulem4  27594  bdaypw2n0bndlem  28632  istrkg2ld  28705  chirred  32713  sbc2iedf  32778  rspc2daf  32779  opreu2reuALT  32789  mo5f  32801  foresf1o  32816  iinabrex  32880  cbvdisjf  32882  disjabrex  32893  disjabrexf  32894  funimass4f  32948  2ndresdju  32960  fmptcof2  32968  fcomptf  32969  acunirnmpt2  32971  acunirnmpt2f  32972  aciunf1lem  32973  funcnv4mpt  32979  fnpreimac  32981  f1od2  33030  fpwrelmap  33044  xrofsup  33078  nn0min  33131  fprodex01  33135  fsumiunle  33139  prodindf  33148  suppgsumssiun  33358  isarchiofld  33485  elrgspnsubrunlem2  33534  nsgqusf1olem1  33688  nsgqusf1olem3  33690  elrspunidl  33702  deg1prod  33839  mplvrpmga  33901  esplyfval1  33929  vieta  33936  fedgmullem2  33986  irngnzply1  34047  reff  34195  locfinreflem  34196  cmpcref  34206  zarclsiin  34227  zarcmplem  34237  ordtconnlem1  34280  esumcl  34386  gsumesum  34415  esumlub  34416  esumcst  34419  esumrnmpt2  34424  esumfzf  34425  esumfsup  34426  hasheuni  34441  esumcvg  34442  esumgect  34446  esumcvgre  34447  esum2dlem  34448  esum2d  34449  esumiun  34450  ldsysgenld  34516  sigapildsyslem  34517  sigapildsys  34518  ldgenpisyslem1  34519  measvunilem  34568  measvunilem0  34569  measvuni  34570  measinblem  34576  voliune  34585  volfiniune  34586  volmeas  34587  oms0  34653  omssubadd  34656  eulerpartlemgvv  34732  dstrvprob  34828  breprexplema  34983  bnj919  35122  bnj1146  35145  bnj1379  35184  bnj849  35279  bnj916  35287  bnj964  35297  bnj1014  35315  bnj1123  35340  bnj1228  35365  bnj1307  35377  bnj1321  35381  bnj1398  35388  bnj1408  35390  bnj1444  35397  bnj1445  35398  bnj1446  35399  bnj1449  35402  bnj1467  35408  bnj1463  35409  bnj1489  35410  bnj1491  35411  bnj1312  35412  bnj1525  35423  dvelimalcased  35429  dvelimexcased  35431  fineqvrep  35493  cvmcov  35721  iota5f  36182  axextdist  36255  axextbdist  36256  nfwlim  36278  finminlem  36795  axtcond  36955  bj-dvelimdv  37452  bj-axreprepsep  37678  bj-opabco  37798  isbasisrelowllem1  37967  isbasisrelowllem2  37968  fvineqsneu  38023  fvineqsneq  38024  wl-cbvalnaed  38153  wl-2sb6d  38179  wl-sbalnae  38183  wl-mo2tf  38192  wl-eutf  38194  phpreu  38221  poimirlem26  38263  poimirlem27  38264  heicant  38272  mbfposadd  38284  ftc1anclem5  38314  indexdom  38351  filbcmb  38357  sdclem2  38359  sdclem1  38360  fdc1  38363  riotasv2d  39699  riotasv2s  39700  nfded2  39710  glbconxN  40120  pmapglb2xN  40514  cdlemefs32sn1aw  41156  mzpsubmpt  43444  mzpexpmpt  43446  eq0rabdioph  43477  eqrabdioph  43478  setindtr  43721  unielss  43915  nadd1suc  44089  ss2iundf  44355  mnuprdlem4  44955  ismnushort  44981  binomcxplemnotnn0  45036  iunconnlem2  45613  nfrelp  45628  modelaxreplem3  45659  modelaxrep  45660  permaxrep  45685  elunif  45706  rspcegf  45713  fnchoice  45719  refsumcn  45720  rfcnnnub  45726  uzwo4  45743  fiiuncl  45755  cbvmpo2  45785  cbvmpo1  45786  iinssiin  45817  disjf1  45871  disjrnmpt2  45876  disjf1o  45879  disjinfi  45880  choicefi  45887  axccdom  45908  dmrelrnrel  45912  axccd  45914  rnmptbddlem  45929  rnmptbd2lem  45933  infnsuprnmpt  45935  rnmptbdlem  45940  rnmptssbi  45945  upbdrech  45994  ssfiunibd  45998  supxrgere  46019  supxrgelem  46023  supxrge  46024  xralrple2  46040  infxr  46052  infxrunb2  46053  xrralrecnnle  46068  xrralrecnnge  46075  supxrunb3  46084  supxrleubrnmpt  46090  infleinf2  46098  unb2ltle  46099  rexabslelem  46102  suprleubrnmpt  46106  uzub  46115  supminfrnmpt  46129  supxrleubrnmptf  46135  infxrgelbrnmpt  46138  infrpgernmpt  46149  monoordxr  46166  monoord2xr  46168  caucvgbf  46173  cvgcaule  46175  iccshift  46204  iooshift  46208  iooiinicc  46228  iooiinioc  46242  fsummulc1f  46257  fsumf1of  46260  fsumreclf  46262  fsumlessf  46263  fmul01  46266  fmuldfeqlem1  46268  fmuldfeq  46269  fmul01lt1lem1  46270  fmul01lt1lem2  46271  fprodexp  46280  mccl  46284  fprodcnlem  46285  fprodcn  46286  climmulf  46290  climexp  46291  climsuse  46294  climrecf  46295  climinff  46297  climaddf  46301  mullimc  46302  islptre  46305  climf  46308  mullimcf  46309  rexlim2d  46311  idlimc  46312  limcperiod  46314  limcrecl  46315  islpcn  46323  limsupre  46325  limcleqr  46328  addlimc  46332  limclner  46335  climsubmpt  46344  climreclf  46348  climf2  46350  climeldmeqmpt  46352  clim2f2  46354  climfveqmpt  46355  fnlimfvre  46358  allbutfifvre  46359  climleltrp  46360  fnlimf  46362  fnlimabslt  46363  climfveqf  46364  climfveqmpt3  46366  climeldmeqf  46367  climeqf  46372  climeldmeqmpt3  46373  limsuppnfd  46386  limsupub  46388  climinf2lem  46390  climinf2  46391  limsuppnf  46395  limsupubuz  46397  climinf2mpt  46398  climinfmpt  46399  climinf3  46400  limsupmnflem  46404  limsupequz  46407  limsupre2  46409  limsupmnfuzlem  46410  limsupequzmptf  46415  limsupre3  46417  limsupre3uzlem  46419  limsupreuzmpt  46423  climisp  46430  lmbr3  46431  climrescn  46432  climxrrelem  46433  climxrre  46434  limsupub2  46496  liminflbuz2  46499  xlimmnfvlem2  46517  xlimmnfv  46518  xlimpnfvlem2  46521  xlimpnfv  46522  xlimmnfmpt  46527  xlimpnfmpt  46528  climxlim2lem  46529  cncficcgt0  46572  cncfioobd  46581  fprodsubrecnncnvlem  46591  fprodaddrecnncnvlem  46593  dvmptmulf  46621  dvnmul  46627  dvmptfprodlem  46628  dvmptfprod  46629  dvnprodlem1  46630  dvnprodlem2  46631  iblsplitf  46654  itgperiod  46665  stoweidlem3  46687  stoweidlem26  46710  stoweidlem27  46711  stoweidlem29  46713  stoweidlem31  46715  stoweidlem34  46718  stoweidlem35  46719  stoweidlem36  46720  stoweidlem39  46723  stoweidlem42  46726  stoweidlem43  46727  stoweidlem44  46728  stoweidlem46  46730  stoweidlem48  46732  stoweidlem49  46733  stoweidlem51  46735  stoweidlem52  46736  stoweidlem53  46737  stoweidlem54  46738  stoweidlem55  46739  stoweidlem56  46740  stoweidlem57  46741  stoweidlem58  46742  stoweidlem59  46743  stoweidlem60  46744  stoweidlem61  46745  stoweidlem62  46746  stoweid  46747  wallispilem3  46751  stirlinglem13  46770  stirling  46773  fourierdlem16  46807  fourierdlem21  46812  fourierdlem22  46813  fourierdlem31  46822  fourierdlem39  46830  fourierdlem48  46838  fourierdlem51  46841  fourierdlem68  46858  fourierdlem71  46861  fourierdlem73  46863  fourierdlem80  46870  fourierdlem81  46871  fourierdlem86  46876  fourierdlem87  46877  fourierdlem93  46883  fourierdlem94  46884  fourierdlem103  46893  fourierdlem104  46894  fourierdlem112  46902  fourierdlem113  46903  elaa2  46918  etransclem32  46950  salexct  47018  sge0revalmpt  47062  sge0f1o  47066  sge0lefi  47082  sge0resplit  47090  sge0lempt  47094  sge0iunmptlemre  47099  sge0fodjrnlem  47100  sge0iunmpt  47102  sge0ltfirpmpt2  47110  sge0isum  47111  sge0xp  47113  sge0isummpt2  47116  sge0xadd  47119  sge0pnffsumgt  47126  sge0gtfsumgt  47127  sge0uzfsumgt  47128  sge0reuz  47131  sge0reuzb  47132  iundjiun  47144  meadjiun  47150  ismeannd  47151  voliunsge0lem  47156  meaiunincf  47167  meaiuninc3v  47168  meaiuninc3  47169  meaiininc  47171  caragenfiiuncl  47199  omeiunltfirp  47203  ovnsubaddlem2  47255  hoidmvval0  47271  hoidmvlelem1  47279  hoidmvlelem3  47281  hoidmvlelem5  47283  ovnlecvr2  47294  hspdifhsp  47300  hoiqssbllem2  47307  hoiqssbllem3  47308  hspmbllem2  47311  opnvonmbllem2  47317  hoimbl2  47349  vonhoire  47356  iinhoiicc  47358  iunhoiioolem  47359  iunhoiioo  47360  vonioo  47366  vonicc  47369  vonn0ioo2  47374  vonn0icc2  47376  salpreimagelt  47391  salpreimalegt  47393  pimincfltioc  47400  pimdecfgtioo  47401  pimincfltioo  47402  preimageiingt  47404  preimaleiinlt  47405  salpreimagtge  47409  salpreimaltle  47410  salpreimalelt  47413  salpreimagtlt  47414  incsmflem  47425  issmflelem  47428  issmfle  47429  smfconst  47433  issmfgtlem  47439  issmfgt  47440  smfaddlem2  47448  smfadd  47449  decsmflem  47450  decsmf  47451  issmfgelem  47453  issmfge  47454  smflimlem2  47456  smflim  47461  smfresal  47472  smfrec  47473  smfmullem4  47478  smfmul  47479  smfpimcc  47492  smflimmpt  47494  smfsuplem1  47495  smfsupmpt  47499  smfsupxr  47500  smfinflem  47501  smfinfmpt  47503  smflimsuplem5  47508  smflimsuplem7  47510  smflimsuplem8  47511  smflimsupmpt  47513  smfliminflem  47514  smfliminfmpt  47516  smfpimne2  47524  fsupdm  47526  smfsupdmmbllem  47528  finfdm  47530  smfinfdmmbllem  47532  or2expropbilem2  47737  or2expropbi  47738  cfsetsnfsetf  47762  2reu8i  47817  nfdfat  47831  iccelpart  48149  ichnfim  48180  ich2exprop  48187  ichreuopeq  48189  sprsymrelfo  48213  reupr  48238  reuopreuprim  48242  2zrngmmgm  48984  cbvmpox2  49083  ovmpordxf  49086  1arymaptfo  49390  2arymaptfo  49401  iinfssclem3  49801  iinfssc  49802  iinfsubc  49803  setrec1  50436  pgindnf  50461  nfals  50548  nfrals  50549  aacllem  50568