Theorem nfan 1931

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

This proof depends on syntax axioms:   ∧ wa 401  ⊤wtru 1570  Ⅎwnf 1815

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

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816

This theorem is used by:  nfnan  1932  nf3an  1933  hban  2333  nfeqf  2410  nfald2  2474  2ax6elem  2499  nfsb4t  2528  nfeu1  2614  eupicka  2659  mopick2  2662  2mo  2673  nfabd2  2945  2ralbida  3285  r19.12  3311  reean  3312  ralcom2  3362  cbvrmow  3390  nfrmow  3394  nfreuw  3395  cbvreu  3404  cbvrabw  3446  nfrabw  3447  cbvrab  3449  ceqsex2  3500  vtocl3gaf  3539  spc2ed  3555  rspce  3565  eqvincf  3603  elrabf  3641  elrab3t  3643  rexab2  3656  morex  3676  reu2  3682  rmo3f  3691  reu2eqd  3693  sbc2iegf  3812  reu8nf  3823  rmo2  3833  rmo3  3835  csbiebt  3875  csbie2t  3884  cbvrabcsfw  3887  cbvreucsf  3890  cbvrabcsf  3891  nfdif  4066  nfin  4121  reusngf  4634  rexreusng  4639  reuprg0  4662  rabsnifsb  4682  nfop  4848  nfopd  4849  eluniab  4880  iuneqconst  4962  cbvopab  5176  cbvopab1  5178  cbvopab1g  5179  cbvopab2  5180  cbvopab1s  5181  mpteq12f  5189  nfmpt  5202  cbvmptf  5204  cbvmptfg  5205  axrep3  5235  axrep5  5238  reusv2lem3  5361  nfpo  5564  nfso  5565  nffr  5623  nfwe  5625  nfxp  5683  opeliunxp  5717  opeliun2xp  5718  nfco  5842  elrnmpt1  5941  nfimad  6064  reuop  6296  iota2  6527  nffun  6562  imadif  6624  nffn  6638  nff  6705  nff1  6776  nffo  6795  nff1o  6822  nffvd  6897  fv3  6903  funimassd  6951  fvmptdf  7000  fompt  7118  f1ossf1o  7129  fmptco  7130  fsnex  7291  nfiso  7330  nfriotadw  7385  cbvriotaw  7386  nfriotad  7388  cbvriota  7390  riota2df  7400  riota5f  7405  oprabv  7480  nfoprab  7484  mpoeq123  7492  nfmpo  7502  cbvoprab1  7507  cbvoprab2  7508  cbvoprab12  7509  cbvoprab3  7511  cbvmpox  7513  ovmpodxf  7570  elovmporab  7667  elovmporab1w  7668  elovmporab1  7669  onminex  7816  fiun  7955  f1iun  7956  opabex3d  7977  opabex3rd  7978  opabex3  7979  dfoprab4f  8067  fmpox  8078  opeliunxp2f  8227  nffrecs  8301  frrlem4  8307  tfr3  8407  tz7.49  8455  naddsuc2  8711  erovlem  8834  nfixpw  8944  nfixp  8945  nfixp1  8946  xpf1o  9158  nneneq  9221  ac6sfi  9275  nfoi  9508  wdom2d  9574  scottabf  9939  setrec1  9972  infpssrlem4  10384  hsmexlem2  10505  hsmexlem4  10507  domtriomlem  10520  axdc3lem2  10529  axdc4lem  10533  zorn2lem4  10577  zorn2lem5  10578  konigthlem  10653  axextnd  10676  axrepndlem2  10678  axrepnd  10679  axunnd  10681  axpowndlem2  10683  axpowndlem4  10685  axpownd  10686  axregndlem2  10688  axregnd  10689  axinfndlem1  10690  axinfnd  10691  zfcndrep  10699  zfcndinf  10703  dedekind  11473  dedekindle  11474  fsuppmapnn0fiublem  14133  fsuppmapnn0fiub  14134  fsuppmapnn0fiubex  14135  reuccatpfxs1  14896  nfsum1  15857  nfsum  15858  fsumclf  15904  fsumsplitf  15908  fsumsplit1  15911  fsum2dlem  15936  fsum00  15965  nfcprod1  16077  nfcprod  16078  fprod2dlem  16147  fprodsplitf  16155  fprodsplit1f  16157  fprodle  16163  lcmfunsnlem1  16812  lcmfunsnlem2lem1  16813  lcmfunsnlem2  16815  mreexexd  17822  acsmapd  18728  gsum2d2lem  20187  dprd2d2  20260  gsummoncoe1  22626  gsummatr01lem4  22973  cpmatmcllem  23036  cayleyhamilton1  23210  neiptopnei  23450  neiptopreu  23451  neitr  23498  iunconnlem  23745  iunconn  23746  ptcnplem  23940  ptcnp  23941  xkocnv  24133  isfildlem  24176  utopsnneiplem  24566  isucn2  24597  cfilucfil  24878  restmetu  24889  ovolfiniun  25822  ovoliunlem3  25825  ovoliunnul  25828  volfiniun  25868  itg2splitlem  26069  itg2split  26070  isibl2  26087  nfitg  26095  cbvitg  26096  limciun  26214  2sqmo  27764  2sqreulem4  27781  bdaypw2n0bndlem  28849  istrkg2ld  28922  chirred  32997  sbc2iedf  33062  rspc2daf  33063  opreu2reuALT  33073  mo5f  33085  foresf1o  33100  iinabrex  33163  cbvdisjf  33165  disjabrex  33176  disjabrexf  33177  funimass4f  33231  2ndresdju  33243  fmptcof2  33251  fcomptf  33252  acunirnmpt2  33254  acunirnmpt2f  33255  aciunf1lem  33256  funcnv4mpt  33262  fnpreimac  33264  f1od2  33311  fpwrelmap  33325  xrofsup  33359  nn0min  33412  fprodex01  33416  fsumiunle  33420  prodindf  33429  suppgsumssiun  33633  isarchiofld  33760  elrgspnsubrunlem2  33809  nsgqusf1olem1  33964  nsgqusf1olem3  33966  elrspunidl  33978  deg1prod  34115  mplvrpmga  34177  esplyfval1  34205  vieta  34212  fedgmullem2  34262  irngnzply1  34323  reff  34471  locfinreflem  34472  cmpcref  34482  zarclsiin  34503  zarcmplem  34513  ordtconnlem1  34556  esumcl  34662  gsumesum  34691  esumlub  34692  esumcst  34695  esumrnmpt2  34700  esumfzf  34701  esumfsup  34702  hasheuni  34717  esumcvg  34718  esumgect  34722  esumcvgre  34723  esum2dlem  34724  esum2d  34725  esumiun  34726  ldsysgenld  34793  sigapildsyslem  34794  sigapildsys  34795  ldgenpisyslem1  34796  measvunilem  34845  measvunilem0  34846  measvuni  34847  measinblem  34853  voliune  34862  volfiniune  34863  volmeas  34864  oms0  34929  omssubadd  34932  eulerpartlemgvv  35008  dstrvprob  35104  breprexplema  35259  bnj919  35398  bnj1146  35421  bnj1379  35460  bnj849  35555  bnj916  35563  bnj964  35573  bnj1014  35591  bnj1123  35616  bnj1228  35641  bnj1307  35653  bnj1321  35657  bnj1398  35664  bnj1408  35666  bnj1444  35673  bnj1445  35674  bnj1446  35675  bnj1449  35678  bnj1467  35684  bnj1463  35685  bnj1489  35686  bnj1491  35687  bnj1312  35688  bnj1525  35699  dvelimalcased  35705  dvelimexcased  35707  fineqvrep  35782  cvmcov  36028  iota5f  36489  axextdist  36561  axextbdist  36562  nfwlim  36584  finminlem  37106  axtcond  37266  mh-inf3f1  37329  bj-dvelimdv  37763  bj-axreprepsep  37991  bj-opabco  38110  isbasisrelowllem1  38279  isbasisrelowllem2  38280  fvineqsneu  38335  fvineqsneq  38336  wl-cbvalnaed  38465  wl-2sb6d  38491  wl-sbalnae  38495  wl-mo2tf  38504  wl-eutf  38506  phpreu  38528  poimirlem26  38565  poimirlem27  38566  heicant  38574  mbfposadd  38586  ftc1anclem5  38616  indexdom  38669  filbcmb  38675  sdclem2  38677  sdclem1  38678  fdc1  38681  riotasv2d  40015  riotasv2s  40016  nfded2  40026  glbconxN  40436  pmapglb2xN  40830  cdlemefs32sn1aw  41472  mzpsubmpt  43754  mzpexpmpt  43756  eq0rabdioph  43787  eqrabdioph  43788  setindtr  44031  unielss  44220  nadd1suc  44394  ss2iundf  44659  mnuprdlem4  45259  ismnushort  45285  binomcxplemnotnn0  45340  iunconnlem2  45917  nfrelp  45939  modelaxreplem3  45970  modelaxrep  45971  permaxrep  45996  elunif  46033  rspcegf  46040  fnchoice  46046  refsumcn  46047  rfcnnnub  46053  uzwo4  46070  fiiuncl  46082  cbvmpo2  46112  cbvmpo1  46113  iinssiin  46144  disjf1  46198  disjrnmpt2  46203  disjf1o  46206  disjinfi  46207  choicefi  46214  axccdom  46235  dmrelrnrel  46239  axccd  46241  rnmptbddlem  46256  rnmptbd2lem  46260  infnsuprnmpt  46262  rnmptbdlem  46267  rnmptssbi  46272  upbdrech  46321  ssfiunibd  46325  supxrgere  46345  supxrgelem  46349  supxrge  46350  xralrple2  46366  infxr  46378  infxrunb2  46379  xrralrecnnle  46394  xrralrecnnge  46401  supxrunb3  46410  supxrleubrnmpt  46416  infleinf2  46424  unb2ltle  46425  rexabslelem  46428  suprleubrnmpt  46432  uzub  46441  supminfrnmpt  46455  supxrleubrnmptf  46461  infxrgelbrnmpt  46464  infrpgernmpt  46475  monoordxr  46492  monoord2xr  46494  caucvgbf  46499  cvgcaule  46501  iccshift  46530  iooshift  46534  iooiinicc  46554  iooiinioc  46568  fsummulc1f  46583  fsumf1of  46586  fsumreclf  46588  fsumlessf  46589  fmul01  46592  fmuldfeqlem1  46594  fmuldfeq  46595  fmul01lt1lem1  46596  fmul01lt1lem2  46597  fprodexp  46606  mccl  46610  fprodcnlem  46611  fprodcn  46612  climmulf  46616  climexp  46617  climsuse  46620  climrecf  46621  climinff  46623  climaddf  46627  mullimc  46628  islptre  46631  climf  46634  mullimcf  46635  rexlim2d  46637  idlimc  46638  limcperiod  46640  limcrecl  46641  islpcn  46649  limsupre  46651  limcleqr  46654  addlimc  46658  limclner  46661  climsubmpt  46670  climreclf  46674  climf2  46676  climeldmeqmpt  46678  clim2f2  46680  climfveqmpt  46681  fnlimfvre  46684  allbutfifvre  46685  climleltrp  46686  fnlimf  46688  fnlimabslt  46689  climfveqf  46690  climfveqmpt3  46692  climeldmeqf  46693  climeqf  46698  climeldmeqmpt3  46699  limsuppnfd  46712  limsupub  46714  climinf2lem  46716  climinf2  46717  limsuppnf  46721  limsupubuz  46723  climinf2mpt  46724  climinfmpt  46725  climinf3  46726  limsupmnflem  46730  limsupequz  46733  limsupre2  46735  limsupmnfuzlem  46736  limsupequzmptf  46741  limsupre3  46743  limsupre3uzlem  46745  limsupreuzmpt  46749  climisp  46756  lmbr3  46757  climrescn  46758  climxrrelem  46759  climxrre  46760  limsupub2  46822  liminflbuz2  46825  xlimmnfvlem2  46843  xlimmnfv  46844  xlimpnfvlem2  46847  xlimpnfv  46848  xlimmnfmpt  46853  xlimpnfmpt  46854  climxlim2lem  46855  cncficcgt0  46898  cncfioobd  46907  fprodsubrecnncnvlem  46917  fprodaddrecnncnvlem  46919  dvmptmulf  46947  dvnmul  46953  dvmptfprodlem  46954  dvmptfprod  46955  dvnprodlem1  46956  dvnprodlem2  46957  iblsplitf  46980  itgperiod  46991  stoweidlem3  47013  stoweidlem26  47036  stoweidlem27  47037  stoweidlem29  47039  stoweidlem31  47041  stoweidlem34  47044  stoweidlem35  47045  stoweidlem36  47046  stoweidlem39  47049  stoweidlem42  47052  stoweidlem43  47053  stoweidlem44  47054  stoweidlem46  47056  stoweidlem48  47058  stoweidlem49  47059  stoweidlem51  47061  stoweidlem52  47062  stoweidlem53  47063  stoweidlem54  47064  stoweidlem55  47065  stoweidlem56  47066  stoweidlem57  47067  stoweidlem58  47068  stoweidlem59  47069  stoweidlem60  47070  stoweidlem61  47071  stoweidlem62  47072  stoweid  47073  wallispilem3  47077  stirlinglem13  47096  stirling  47099  fourierdlem16  47133  fourierdlem21  47138  fourierdlem22  47139  fourierdlem31  47148  fourierdlem39  47156  fourierdlem48  47164  fourierdlem51  47167  fourierdlem68  47184  fourierdlem71  47187  fourierdlem73  47189  fourierdlem80  47196  fourierdlem81  47197  fourierdlem86  47202  fourierdlem87  47203  fourierdlem93  47209  fourierdlem94  47210  fourierdlem103  47219  fourierdlem104  47220  fourierdlem112  47228  fourierdlem113  47229  elaa2  47244  etransclem32  47276  salexct  47344  sge0revalmpt  47388  sge0f1o  47392  sge0lefi  47408  sge0resplit  47416  sge0lempt  47420  sge0iunmptlemre  47425  sge0fodjrnlem  47426  sge0iunmpt  47428  sge0ltfirpmpt2  47436  sge0isum  47437  sge0xp  47439  sge0isummpt2  47442  sge0xadd  47445  sge0pnffsumgt  47452  sge0gtfsumgt  47453  sge0uzfsumgt  47454  sge0reuz  47457  sge0reuzb  47458  iundjiun  47470  meadjiun  47476  ismeannd  47477  voliunsge0lem  47482  meaiunincf  47493  meaiuninc3v  47494  meaiuninc3  47495  meaiininc  47497  caragenfiiuncl  47525  omeiunltfirp  47529  ovnsubaddlem2  47581  hoidmvval0  47597  hoidmvlelem1  47605  hoidmvlelem3  47607  hoidmvlelem5  47609  ovnlecvr2  47620  hspdifhsp  47626  hoiqssbllem2  47633  hoiqssbllem3  47634  hspmbllem2  47637  opnvonmbllem2  47643  hoimbl2  47675  vonhoire  47682  iinhoiicc  47684  iunhoiioolem  47685  iunhoiioo  47686  vonioo  47692  vonicc  47695  vonn0ioo2  47700  vonn0icc2  47702  salpreimagelt  47717  salpreimalegt  47719  pimincfltioc  47726  pimdecfgtioo  47727  pimincfltioo  47728  preimageiingt  47730  preimaleiinlt  47731  salpreimagtge  47735  salpreimaltle  47736  salpreimalelt  47739  salpreimagtlt  47740  incsmflem  47751  issmflelem  47754  issmfle  47755  smfconst  47759  issmfgtlem  47765  issmfgt  47766  smfaddlem2  47774  smfadd  47775  decsmflem  47776  decsmf  47777  issmfgelem  47779  issmfge  47780  smflimlem2  47782  smflim  47787  smfresal  47798  smfrec  47799  smfmullem4  47804  smfmul  47805  smfpimcc  47818  smflimmpt  47820  smfsuplem1  47821  smfsupmpt  47825  smfsupxr  47826  smfinflem  47827  smfinfmpt  47829  smflimsuplem5  47834  smflimsuplem7  47836  smflimsuplem8  47837  smflimsupmpt  47839  smfliminflem  47840  smfliminfmpt  47842  smfpimne2  47850  fsupdm  47852  smfsupdmmbllem  47854  finfdm  47856  smfinfdmmbllem  47858  or2expropbilem2  48103  or2expropbi  48104  cfsetsnfsetf  48128  2reu8i  48183  nfdfat  48197  iccelpart  48515  ichnfim  48546  ich2exprop  48553  ichreuopeq  48555  sprsymrelfo  48579  reupr  48604  reuopreuprim  48608  2zrngmmgm  49349  cbvmpox2  49448  ovmpordxf  49451  1arymaptfo  49755  2arymaptfo  49766  iinfssclem3  50164  iinfssc  50165  iinfsubc  50166  pgindnf  50809  nfals  50899  nfrals  50900  nfalseu  50930  nfralseu  50931  aacllem  50939