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  3260  r19.12  3286  reean  3287  ralcom2  3348  cbvrmow  3376  nfrmow  3380  nfreuw  3381  cbvreu  3392  cbvrabw  3435  cbvrabwOLD  3436  nfrabw  3437  cbvrab  3440  ceqsex2  3494  vtocl2gafOLD  3536  vtocl3gaf  3537  spc2ed  3556  rspce  3566  eqvincf  3605  elrabf  3644  elrab3t  3646  rexab2  3658  morex  3678  reu2  3684  rmo3f  3693  reu2eqd  3695  sbc2iegf  3816  reu8nf  3828  rmo2  3838  rmo3  3840  csbiebt  3879  csbie2t  3888  cbvrabcsfw  3891  cbvreucsf  3894  cbvrabcsf  3895  nfdif  4082  nfin  4177  reusngf  4632  rexreusng  4637  reuprg0  4660  rabsnifsb  4680  nfop  4846  nfopd  4847  eluniab  4878  iuneqconst  4959  cbvopab  5171  cbvopab1  5173  cbvopab1g  5174  cbvopab2  5175  cbvopab1s  5176  mpteq12f  5184  nfmpt  5197  cbvmptf  5199  cbvmptfg  5200  axrep3  5229  axrep4OLD  5232  axrep5  5233  reusv2lem3  5346  axprlem4OLD  5375  axprlem5OLD  5376  nfpo  5539  nfso  5540  nffr  5598  nfwe  5600  nfxp  5658  opeliunxp  5692  opeliun2xp  5693  nfco  5815  elrnmpt1  5910  nfimad  6029  reuop  6252  iota2  6482  nffun  6516  imadif  6577  nffn  6592  nff  6659  nff1  6729  nffo  6746  nff1o  6773  nffvd  6847  fv3  6853  funimassd  6901  fvmptdf  6949  fompt  7065  f1ossf1o  7075  fmptco  7076  fsnex  7231  nfiso  7270  nfriotadw  7325  cbvriotaw  7326  nfriotad  7328  cbvriota  7330  riota2df  7340  riota5f  7345  oprabv  7420  nfoprab  7424  mpoeq123  7432  nfmpo  7442  cbvoprab1  7447  cbvoprab2  7448  cbvoprab12  7449  cbvoprab3  7451  cbvmpox  7453  ovmpodxf  7510  elovmporab  7606  elovmporab1w  7607  elovmporab1  7608  onminex  7749  fiun  7889  f1iun  7890  opabex3d  7911  opabex3rd  7912  opabex3  7913  dfoprab4f  8002  fmpox  8013  opeliunxp2f  8154  nffrecs  8227  frrlem4  8233  tfr3  8332  tz7.49  8378  naddsuc2  8631  erovlem  8754  nfixpw  8858  nfixp  8859  nfixp1  8860  xpf1o  9071  nneneq  9134  ac6sfi  9188  nfoi  9423  wdom2d  9489  infpssrlem4  10220  hsmexlem2  10341  hsmexlem4  10343  domtriomlem  10356  axdc3lem2  10365  axdc4lem  10369  zorn2lem4  10413  zorn2lem5  10414  konigthlem  10483  axextnd  10506  axrepndlem2  10508  axrepnd  10509  axunnd  10511  axpowndlem2  10513  axpowndlem4  10515  axpownd  10516  axregndlem2  10518  axregnd  10519  axinfndlem1  10520  axinfnd  10521  zfcndrep  10529  zfcndinf  10533  dedekind  11300  dedekindle  11301  fsuppmapnn0fiublem  13917  fsuppmapnn0fiub  13918  fsuppmapnn0fiubex  13919  reuccatpfxs1  14674  nfsum1  15617  nfsum  15618  fsumclf  15665  fsumsplitf  15669  fsumsplit1  15672  fsum2dlem  15697  fsum00  15725  nfcprod1  15835  nfcprod  15836  fprod2dlem  15907  fprodsplitf  15915  fprodsplit1f  15917  fprodle  15923  lcmfunsnlem1  16568  lcmfunsnlem2lem1  16569  lcmfunsnlem2  16571  mreexexd  17575  acsmapd  18481  gsum2d2lem  19906  dprd2d2  19979  gsummoncoe1  22256  gsummatr01lem4  22606  cpmatmcllem  22666  cayleyhamilton1  22840  neiptopnei  23080  neiptopreu  23081  neitr  23128  iunconnlem  23375  iunconn  23376  ptcnplem  23569  ptcnp  23570  xkocnv  23762  isfildlem  23805  utopsnneiplem  24195  isucn2  24226  cfilucfil  24507  restmetu  24518  ovolfiniun  25462  ovoliunlem3  25465  ovoliunnul  25468  volfiniun  25508  itg2splitlem  25709  itg2split  25710  isibl2  25727  nfitg  25736  cbvitg  25737  limciun  25855  2sqmo  27408  2sqreulem4  27425  bdaypw2n0sbndlem  28442  istrkg2ld  28515  chirred  32453  sbc2iedf  32521  rspc2daf  32522  opreu2reuALT  32533  mo5f  32545  foresf1o  32561  iinabrex  32626  cbvdisjf  32628  disjabrex  32639  disjabrexf  32640  funimass4f  32697  2ndresdju  32709  fmptcof2  32717  fcomptf  32718  acunirnmpt2  32720  acunirnmpt2f  32721  aciunf1lem  32722  funcnv4mpt  32728  fnpreimac  32730  f1od2  32779  fpwrelmap  32793  xrofsup  32828  nn0min  32882  fprodex01  32887  fsumiunle  32891  prodindf  32925  isarchiofld  33262  elrgspnsubrunlem2  33311  nsgqusf1olem1  33475  nsgqusf1olem3  33477  elrspunidl  33490  deg1prod  33645  mplvrpmga  33691  vieta  33717  fedgmullem2  33768  irngnzply1  33829  reff  33977  locfinreflem  33978  cmpcref  33988  zarclsiin  34009  zarcmplem  34019  ordtconnlem1  34062  esumcl  34168  gsumesum  34197  esumlub  34198  esumcst  34201  esumrnmpt2  34206  esumfzf  34207  esumfsup  34208  hasheuni  34223  esumcvg  34224  esumgect  34228  esumcvgre  34229  esum2dlem  34230  esum2d  34231  esumiun  34232  ldsysgenld  34298  sigapildsyslem  34299  sigapildsys  34300  ldgenpisyslem1  34301  measvunilem  34350  measvunilem0  34351  measvuni  34352  measinblem  34358  voliune  34367  volfiniune  34368  volmeas  34369  oms0  34435  omssubadd  34438  eulerpartlemgvv  34514  dstrvprob  34610  breprexplema  34768  bnj919  34904  bnj1146  34928  bnj1379  34967  bnj849  35062  bnj916  35070  bnj964  35080  bnj1014  35098  bnj1123  35123  bnj1228  35148  bnj1307  35160  bnj1321  35164  bnj1398  35171  bnj1408  35173  bnj1444  35180  bnj1445  35181  bnj1446  35182  bnj1449  35185  bnj1467  35191  bnj1463  35192  bnj1489  35193  bnj1491  35194  bnj1312  35195  bnj1525  35206  dvelimalcased  35212  dvelimexcased  35214  fineqvrep  35251  cvmcov  35438  iota5f  35899  axextdist  35972  axextbdist  35973  nfwlim  35995  finminlem  36493  bj-dvelimdv  37027  bj-opabco  37364  isbasisrelowllem1  37531  isbasisrelowllem2  37532  fvineqsneu  37587  fvineqsneq  37588  wl-cbvalnaed  37708  wl-2sb6d  37734  wl-sbalnae  37738  wl-mo2tf  37747  wl-eutf  37749  phpreu  37776  poimirlem26  37818  poimirlem27  37819  heicant  37827  mbfposadd  37839  ftc1anclem5  37869  indexdom  37906  filbcmb  37912  sdclem2  37914  sdclem1  37915  fdc1  37918  riotasv2d  39254  riotasv2s  39255  nfded2  39265  glbconxN  39675  pmapglb2xN  40069  cdlemefs32sn1aw  40711  mzpsubmpt  43021  mzpexpmpt  43023  eq0rabdioph  43054  eqrabdioph  43055  setindtr  43302  unielss  43496  nadd1suc  43670  ss2iundf  43936  scottabf  44517  mnuprdlem4  44552  ismnushort  44578  binomcxplemnotnn0  44633  iunconnlem2  45211  nfrelp  45226  modelaxreplem3  45257  modelaxrep  45258  permaxrep  45283  elunif  45297  rspcegf  45304  fnchoice  45310  refsumcn  45311  rfcnnnub  45317  uzwo4  45334  fiiuncl  45346  cbvmpo2  45377  cbvmpo1  45378  iinssiin  45409  disjf1  45463  disjrnmpt2  45468  disjf1o  45471  disjinfi  45472  choicefi  45480  axccdom  45502  dmrelrnrel  45506  axccd  45509  rnmptbddlem  45524  rnmptbd2lem  45528  infnsuprnmpt  45530  rnmptbdlem  45535  rnmptssbi  45540  upbdrech  45589  ssfiunibd  45593  supxrgere  45614  supxrgelem  45618  supxrge  45619  xralrple2  45635  infxr  45647  infxrunb2  45648  xrralrecnnle  45663  xrralrecnnge  45670  supxrunb3  45679  supxrleubrnmpt  45686  infleinf2  45694  unb2ltle  45695  rexabslelem  45698  suprleubrnmpt  45702  uzub  45711  supminfrnmpt  45725  supxrleubrnmptf  45731  infxrgelbrnmpt  45734  infrpgernmpt  45745  monoordxr  45762  monoord2xr  45764  caucvgbf  45769  cvgcaule  45771  iccshift  45800  iooshift  45804  iooiinicc  45824  iooiinioc  45838  fsummulc1f  45853  fsumf1of  45856  fsumreclf  45858  fsumlessf  45859  fmul01  45862  fmuldfeqlem1  45864  fmuldfeq  45865  fmul01lt1lem1  45866  fmul01lt1lem2  45867  fprodexp  45876  mccl  45880  fprodcnlem  45881  fprodcn  45882  climmulf  45886  climexp  45887  climsuse  45890  climrecf  45891  climinff  45893  climaddf  45897  mullimc  45898  islptre  45901  climf  45904  mullimcf  45905  rexlim2d  45907  idlimc  45908  limcperiod  45910  limcrecl  45911  islpcn  45919  limsupre  45921  limcleqr  45924  addlimc  45928  limclner  45931  climsubmpt  45940  climreclf  45944  climf2  45946  climeldmeqmpt  45948  clim2f2  45950  climfveqmpt  45951  fnlimfvre  45954  allbutfifvre  45955  climleltrp  45956  fnlimf  45958  fnlimabslt  45959  climfveqf  45960  climfveqmpt3  45962  climeldmeqf  45963  climeqf  45968  climeldmeqmpt3  45969  limsuppnfd  45982  limsupub  45984  climinf2lem  45986  climinf2  45987  limsuppnf  45991  limsupubuz  45993  climinf2mpt  45994  climinfmpt  45995  climinf3  45996  limsupmnflem  46000  limsupequz  46003  limsupre2  46005  limsupmnfuzlem  46006  limsupequzmptf  46011  limsupre3  46013  limsupre3uzlem  46015  limsupreuzmpt  46019  climisp  46026  lmbr3  46027  climrescn  46028  climxrrelem  46029  climxrre  46030  limsupub2  46092  liminflbuz2  46095  xlimmnfvlem2  46113  xlimmnfv  46114  xlimpnfvlem2  46117  xlimpnfv  46118  xlimmnfmpt  46123  xlimpnfmpt  46124  climxlim2lem  46125  cncficcgt0  46168  cncfioobd  46177  fprodsubrecnncnvlem  46187  fprodaddrecnncnvlem  46189  dvmptmulf  46217  dvnmul  46223  dvmptfprodlem  46224  dvmptfprod  46225  dvnprodlem1  46226  dvnprodlem2  46227  iblsplitf  46250  itgperiod  46261  stoweidlem3  46283  stoweidlem26  46306  stoweidlem27  46307  stoweidlem29  46309  stoweidlem31  46311  stoweidlem34  46314  stoweidlem35  46315  stoweidlem36  46316  stoweidlem39  46319  stoweidlem42  46322  stoweidlem43  46323  stoweidlem44  46324  stoweidlem46  46326  stoweidlem48  46328  stoweidlem49  46329  stoweidlem51  46331  stoweidlem52  46332  stoweidlem53  46333  stoweidlem54  46334  stoweidlem55  46335  stoweidlem56  46336  stoweidlem57  46337  stoweidlem58  46338  stoweidlem59  46339  stoweidlem60  46340  stoweidlem61  46341  stoweidlem62  46342  stoweid  46343  wallispilem3  46347  stirlinglem13  46366  stirling  46369  fourierdlem16  46403  fourierdlem21  46408  fourierdlem22  46409  fourierdlem31  46418  fourierdlem39  46426  fourierdlem48  46434  fourierdlem51  46437  fourierdlem68  46454  fourierdlem71  46457  fourierdlem73  46459  fourierdlem80  46466  fourierdlem81  46467  fourierdlem86  46472  fourierdlem87  46473  fourierdlem93  46479  fourierdlem94  46480  fourierdlem103  46489  fourierdlem104  46490  fourierdlem112  46498  fourierdlem113  46499  elaa2  46514  etransclem32  46546  salexct  46614  sge0revalmpt  46658  sge0f1o  46662  sge0lefi  46678  sge0resplit  46686  sge0lempt  46690  sge0iunmptlemre  46695  sge0fodjrnlem  46696  sge0iunmpt  46698  sge0ltfirpmpt2  46706  sge0isum  46707  sge0xp  46709  sge0isummpt2  46712  sge0xadd  46715  sge0pnffsumgt  46722  sge0gtfsumgt  46723  sge0uzfsumgt  46724  sge0reuz  46727  sge0reuzb  46728  iundjiun  46740  meadjiun  46746  ismeannd  46747  voliunsge0lem  46752  meaiunincf  46763  meaiuninc3v  46764  meaiuninc3  46765  meaiininc  46767  caragenfiiuncl  46795  omeiunltfirp  46799  ovnsubaddlem2  46851  hoidmvval0  46867  hoidmvlelem1  46875  hoidmvlelem3  46877  hoidmvlelem5  46879  ovnlecvr2  46890  hspdifhsp  46896  hoiqssbllem2  46903  hoiqssbllem3  46904  hspmbllem2  46907  opnvonmbllem2  46913  hoimbl2  46945  vonhoire  46952  iinhoiicc  46954  iunhoiioolem  46955  iunhoiioo  46956  vonioo  46962  vonicc  46965  vonn0ioo2  46970  vonn0icc2  46972  salpreimagelt  46987  salpreimalegt  46989  pimincfltioc  46996  pimdecfgtioo  46997  pimincfltioo  46998  preimageiingt  47000  preimaleiinlt  47001  salpreimagtge  47005  salpreimaltle  47006  salpreimalelt  47009  salpreimagtlt  47010  incsmflem  47021  issmflelem  47024  issmfle  47025  smfconst  47029  issmfgtlem  47035  issmfgt  47036  smfaddlem2  47044  smfadd  47045  decsmflem  47046  decsmf  47047  issmfgelem  47049  issmfge  47050  smflimlem2  47052  smflim  47057  smfresal  47068  smfrec  47069  smfmullem4  47074  smfmul  47075  smfpimcc  47088  smflimmpt  47090  smfsuplem1  47091  smfsupmpt  47095  smfsupxr  47096  smfinflem  47097  smfinfmpt  47099  smflimsuplem5  47104  smflimsuplem7  47106  smflimsuplem8  47107  smflimsupmpt  47109  smfliminflem  47110  smfliminfmpt  47112  smfpimne2  47120  fsupdm  47122  smfsupdmmbllem  47124  finfdm  47126  smfinfdmmbllem  47128  or2expropbilem2  47315  or2expropbi  47316  cfsetsnfsetf  47340  2reu8i  47395  nfdfat  47409  iccelpart  47715  ichnfim  47746  ich2exprop  47753  ichreuopeq  47755  sprsymrelfo  47779  reupr  47804  reuopreuprim  47808  2zrngmmgm  48534  cbvmpox2  48618  ovmpordxf  48621  1arymaptfo  48925  2arymaptfo  48936  iinfssclem3  49337  iinfssc  49338  iinfsubc  49339  setrec1  49972  pgindnf  49997  aacllem  50082