Theorem nfan 1902

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

Syntax hints:   ∧ wa 396  ⊤wtru 1542  Ⅎ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 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfnan  1903  nf3an  1904  hban  2296  nfeqf  2380  nfald2  2444  2ax6elem  2469  nfsb4t  2498  nfeu1ALT  2583  eupicka  2630  mopick2  2633  2mo  2644  clelabOLD  2880  nfabd2  2929  2ralbida  3280  r19.12  3311  r19.12OLD  3312  reean  3313  ralcom2  3373  cbvrmow  3405  nfrmow  3409  nfreuw  3410  cbvreuwOLD  3412  cbvreu  3424  cbvrabw  3467  nfrabw  3468  cbvrab  3473  ceqsex2  3529  vtocl2gaf  3567  spc2ed  3591  rspce  3601  eqvincf  3638  elrabf  3679  elrab3t  3682  rexab2  3695  morex  3715  reu2  3721  rmo3f  3730  reu2eqd  3732  sbc2iegf  3859  reu8nf  3871  rmo2  3881  rmo3  3883  csbiebt  3923  csbie2t  3934  cbvrabcsfw  3937  cbvreucsf  3940  cbvrabcsf  3941  reusngf  4676  rexreusng  4683  reuprg0  4706  rabsnifsb  4726  nfop  4889  nfopd  4890  eluniab  4923  iuneqconst  5008  cbvopab  5220  cbvopab1  5223  cbvopab1g  5224  cbvopab2  5225  cbvopab1s  5226  mpteq12f  5236  nfmpt  5255  cbvmptf  5257  cbvmptfg  5258  axrep3  5289  axrep4  5290  axrep5  5291  reusv2lem3  5398  axprlem4  5424  axprlem5  5425  nfpo  5593  nfso  5594  nffr  5650  nfwe  5652  nfxp  5709  opeliunxp  5743  nfco  5865  elrnmpt1  5957  nfimad  6068  reuop  6292  iota2  6532  nffun  6571  imadif  6632  nffn  6648  nff  6713  nff1  6785  nffo  6804  nff1o  6831  nffvd  6903  fv3  6909  funimassd  6958  fvmptdf  7004  f1ossf1o  7125  fmptco  7126  fsnex  7280  nfiso  7318  nfriotadw  7372  cbvriotaw  7373  nfriotad  7376  cbvriota  7378  riota2df  7388  riota5f  7393  oprabv  7468  nfoprab  7472  mpoeq123  7480  nfmpo  7490  cbvoprab1  7495  cbvoprab2  7496  cbvoprab12  7497  cbvoprab3  7499  cbvmpox  7501  ovmpodxf  7557  elovmporab  7651  elovmporab1w  7652  elovmporab1  7653  onminex  7789  peano5OLD  7884  fiun  7928  f1iun  7929  opabex3d  7951  opabex3rd  7952  opabex3  7953  dfoprab4f  8041  fmpox  8052  opeliunxp2f  8194  nffrecs  8267  frrlem4  8273  nfwrecsOLD  8301  wfrlem4OLD  8311  tfr3  8398  tz7.49  8444  erovlem  8806  nfixpw  8909  nfixp  8910  nfixp1  8911  xpf1o  9138  nneneq  9208  nneneqOLD  9220  ac6sfi  9286  nfoi  9508  wdom2d  9574  infpssrlem4  10300  hsmexlem2  10421  hsmexlem4  10423  domtriomlem  10436  axdc3lem2  10445  axdc4lem  10449  zorn2lem4  10493  zorn2lem5  10494  konigthlem  10562  axextnd  10585  axrepndlem2  10587  axrepnd  10588  axunnd  10590  axpowndlem2  10592  axpowndlem4  10594  axpownd  10595  axregndlem2  10597  axregnd  10598  axinfndlem1  10599  axinfnd  10600  zfcndrep  10608  zfcndinf  10612  dedekind  11376  dedekindle  11377  fsuppmapnn0fiublem  13954  fsuppmapnn0fiub  13955  fsuppmapnn0fiubex  13956  reuccatpfxs1  14696  nfsum1  15635  nfsum  15636  fsumclf  15683  fsumsplitf  15687  fsumsplit1  15690  fsum2dlem  15715  fsum00  15743  nfcprod1  15853  nfcprod  15854  fprod2dlem  15923  fprodsplitf  15931  fprodsplit1f  15933  fprodle  15939  lcmfunsnlem1  16573  lcmfunsnlem2lem1  16574  lcmfunsnlem2  16576  mreexexd  17591  acsmapd  18506  gsum2d2lem  19840  dprd2d2  19913  gsummoncoe1  21827  gsummatr01lem4  22159  cpmatmcllem  22219  cayleyhamilton1  22393  neiptopnei  22635  neiptopreu  22636  neitr  22683  iunconnlem  22930  iunconn  22931  ptcnplem  23124  ptcnp  23125  xkocnv  23317  isfildlem  23360  utopsnneiplem  23751  isucn2  23783  cfilucfil  24067  restmetu  24078  ovolfiniun  25017  ovoliunlem3  25020  ovoliunnul  25023  volfiniun  25063  itg2splitlem  25265  itg2split  25266  isibl2  25283  nfitg  25291  cbvitg  25292  limciun  25410  2sqmo  26937  2sqreulem4  26954  istrkg2ld  27708  chirred  31643  sbc2iedf  31702  rspc2daf  31703  opreu2reuALT  31712  mo5f  31724  foresf1o  31737  iinabrex  31795  cbvdisjf  31797  disjabrex  31808  disjabrexf  31809  funimass4f  31856  2ndresdju  31869  fmptcof2  31877  fcomptf  31878  acunirnmpt2  31880  acunirnmpt2f  31881  aciunf1lem  31882  funcnv4mpt  31889  fnpreimac  31891  cnvoprabOLD  31940  f1od2  31941  fpwrelmap  31953  xrofsup  31975  nn0min  32021  fprodex01  32026  fsumiunle  32030  isarchiofld  32430  nsgqusf1olem1  32519  nsgqusf1olem3  32521  elrspunidl  32541  fedgmullem2  32710  irngnzply1  32750  reff  32814  locfinreflem  32815  cmpcref  32825  zarclsiin  32846  zarcmplem  32856  ordtconnlem1  32899  prodindf  33016  esumcl  33023  gsumesum  33052  esumlub  33053  esumcst  33056  esumrnmpt2  33061  esumfzf  33062  esumfsup  33063  hasheuni  33078  esumcvg  33079  esumgect  33083  esumcvgre  33084  esum2dlem  33085  esum2d  33086  esumiun  33087  ldsysgenld  33153  sigapildsyslem  33154  sigapildsys  33155  ldgenpisyslem1  33156  measvunilem  33205  measvunilem0  33206  measvuni  33207  measinblem  33213  voliune  33222  volfiniune  33223  volmeas  33224  oms0  33291  omssubadd  33294  eulerpartlemgvv  33370  dstrvprob  33465  breprexplema  33637  bnj919  33773  bnj1146  33797  bnj1379  33836  bnj849  33931  bnj916  33939  bnj964  33949  bnj1014  33967  bnj1123  33992  bnj1228  34017  bnj1307  34029  bnj1321  34033  bnj1398  34040  bnj1408  34042  bnj1444  34049  bnj1445  34050  bnj1446  34051  bnj1449  34054  bnj1467  34060  bnj1463  34061  bnj1489  34062  bnj1491  34063  bnj1312  34064  bnj1525  34075  fineqvrep  34090  cvmcov  34249  iota5f  34688  axextdist  34766  axextbdist  34767  nfwlim  34789  finminlem  35198  bj-dvelimdv  35725  bj-opabco  36064  isbasisrelowllem1  36231  isbasisrelowllem2  36232  fvineqsneu  36287  fvineqsneq  36288  wl-cbvalnaed  36396  wl-2sb6d  36418  wl-sbalnae  36422  wl-mo2tf  36431  wl-eutf  36433  wl-ax11-lem3  36444  phpreu  36467  poimirlem26  36509  poimirlem27  36510  heicant  36518  mbfposadd  36530  ftc1anclem5  36560  indexdom  36597  filbcmb  36603  sdclem2  36605  sdclem1  36606  fdc1  36609  riotasv2d  37822  riotasv2s  37823  nfded2  37833  glbconxN  38244  pmapglb2xN  38638  cdlemefs32sn1aw  39280  mzpsubmpt  41471  mzpexpmpt  41473  eq0rabdioph  41504  eqrabdioph  41505  setindtr  41753  unielss  41957  nadd1suc  42132  naddsuc2  42133  ss2iundf  42400  scottabf  42989  mnuprdlem4  43024  ismnushort  43050  binomcxplemnotnn0  43105  iunconnlem2  43686  elunif  43690  rspcegf  43697  fnchoice  43703  refsumcn  43704  rfcnnnub  43710  uzwo4  43730  fiiuncl  43742  cbvmpo2  43776  cbvmpo1  43777  iinssiin  43808  disjf1  43870  disjrnmpt2  43876  disjf1o  43879  fompt  43880  disjinfi  43881  choicefi  43889  axccdom  43911  dmrelrnrel  43915  axccd  43918  rnmptbddlem  43938  rnmptbd2lem  43942  infnsuprnmpt  43944  rnmptbdlem  43949  rnmptssbi  43955  upbdrech  44005  ssfiunibd  44009  supxrgere  44033  supxrgelem  44037  supxrge  44038  xralrple2  44054  infxr  44067  infxrunb2  44068  xrralrecnnle  44083  xrralrecnnge  44090  supxrunb3  44099  supxrleubrnmpt  44106  infleinf2  44114  unb2ltle  44115  rexabslelem  44118  suprleubrnmpt  44122  uzub  44131  supminfrnmpt  44145  supxrleubrnmptf  44151  infxrgelbrnmpt  44154  infrpgernmpt  44165  monoordxr  44183  monoord2xr  44185  caucvgbf  44190  cvgcaule  44192  iccshift  44221  iooshift  44225  iooiinicc  44245  iooiinioc  44259  fsummulc1f  44277  fsumf1of  44280  fsumreclf  44282  fsumlessf  44283  fmul01  44286  fmuldfeqlem1  44288  fmuldfeq  44289  fmul01lt1lem1  44290  fmul01lt1lem2  44291  fprodexp  44300  mccl  44304  fprodcnlem  44305  fprodcn  44306  climmulf  44310  climexp  44311  climsuse  44314  climrecf  44315  climinff  44317  climaddf  44321  mullimc  44322  islptre  44325  climf  44328  mullimcf  44329  rexlim2d  44331  idlimc  44332  limcperiod  44334  limcrecl  44335  islpcn  44345  limsupre  44347  limcleqr  44350  addlimc  44354  limclner  44357  climsubmpt  44366  climreclf  44370  climf2  44372  climeldmeqmpt  44374  clim2f2  44376  climfveqmpt  44377  fnlimfvre  44380  allbutfifvre  44381  climleltrp  44382  fnlimf  44384  fnlimabslt  44385  climfveqf  44386  climfveqmpt3  44388  climeldmeqf  44389  climeqf  44394  climeldmeqmpt3  44395  limsuppnfd  44408  limsupub  44410  climinf2lem  44412  climinf2  44413  limsuppnf  44417  limsupubuz  44419  climinf2mpt  44420  climinfmpt  44421  climinf3  44422  limsupmnflem  44426  limsupequz  44429  limsupre2  44431  limsupmnfuzlem  44432  limsupequzmptf  44437  limsupre3  44439  limsupre3uzlem  44441  limsupreuzmpt  44445  climisp  44452  lmbr3  44453  climrescn  44454  climxrrelem  44455  climxrre  44456  limsupub2  44518  liminflbuz2  44521  xlimmnfvlem2  44539  xlimmnfv  44540  xlimpnfvlem2  44543  xlimpnfv  44544  xlimmnfmpt  44549  xlimpnfmpt  44550  climxlim2lem  44551  cncficcgt0  44594  cncfioobd  44603  fprodsubrecnncnvlem  44613  fprodaddrecnncnvlem  44615  dvmptmulf  44643  dvnmul  44649  dvmptfprodlem  44650  dvmptfprod  44651  dvnprodlem1  44652  dvnprodlem2  44653  iblsplitf  44676  itgperiod  44687  stoweidlem3  44709  stoweidlem26  44732  stoweidlem27  44733  stoweidlem29  44735  stoweidlem31  44737  stoweidlem34  44740  stoweidlem35  44741  stoweidlem36  44742  stoweidlem39  44745  stoweidlem42  44748  stoweidlem43  44749  stoweidlem44  44750  stoweidlem46  44752  stoweidlem48  44754  stoweidlem49  44755  stoweidlem51  44757  stoweidlem52  44758  stoweidlem53  44759  stoweidlem54  44760  stoweidlem55  44761  stoweidlem56  44762  stoweidlem57  44763  stoweidlem58  44764  stoweidlem59  44765  stoweidlem60  44766  stoweidlem61  44767  stoweidlem62  44768  stoweid  44769  wallispilem3  44773  stirlinglem13  44792  stirling  44795  fourierdlem16  44829  fourierdlem21  44834  fourierdlem22  44835  fourierdlem31  44844  fourierdlem39  44852  fourierdlem48  44860  fourierdlem51  44863  fourierdlem68  44880  fourierdlem71  44883  fourierdlem73  44885  fourierdlem80  44892  fourierdlem81  44893  fourierdlem86  44898  fourierdlem87  44899  fourierdlem93  44905  fourierdlem94  44906  fourierdlem103  44915  fourierdlem104  44916  fourierdlem112  44924  fourierdlem113  44925  elaa2  44940  etransclem32  44972  salexct  45040  sge0revalmpt  45084  sge0f1o  45088  sge0lefi  45104  sge0resplit  45112  sge0lempt  45116  sge0iunmptlemre  45121  sge0fodjrnlem  45122  sge0iunmpt  45124  sge0ltfirpmpt2  45132  sge0isum  45133  sge0xp  45135  sge0isummpt2  45138  sge0xadd  45141  sge0pnffsumgt  45148  sge0gtfsumgt  45149  sge0uzfsumgt  45150  sge0reuz  45153  sge0reuzb  45154  iundjiun  45166  meadjiun  45172  ismeannd  45173  voliunsge0lem  45178  meaiunincf  45189  meaiuninc3v  45190  meaiuninc3  45191  meaiininc  45193  caragenfiiuncl  45221  omeiunltfirp  45225  ovnsubaddlem2  45277  hoidmvval0  45293  hoidmvlelem1  45301  hoidmvlelem3  45303  hoidmvlelem5  45305  ovnlecvr2  45316  hspdifhsp  45322  hoiqssbllem2  45329  hoiqssbllem3  45330  hspmbllem2  45333  opnvonmbllem2  45339  hoimbl2  45371  vonhoire  45378  iinhoiicc  45380  iunhoiioolem  45381  iunhoiioo  45382  vonioo  45388  vonicc  45391  vonn0ioo2  45396  vonn0icc2  45398  salpreimagelt  45413  salpreimalegt  45415  pimincfltioc  45422  pimdecfgtioo  45423  pimincfltioo  45424  preimageiingt  45426  preimaleiinlt  45427  salpreimagtge  45431  salpreimaltle  45432  salpreimalelt  45435  salpreimagtlt  45436  incsmflem  45447  issmflelem  45450  issmfle  45451  smfconst  45455  issmfgtlem  45461  issmfgt  45462  smfaddlem2  45470  smfadd  45471  decsmflem  45472  decsmf  45473  issmfgelem  45475  issmfge  45476  smflimlem2  45478  smflim  45483  smfresal  45494  smfrec  45495  smfmullem4  45500  smfmul  45501  smfpimcc  45514  smflimmpt  45516  smfsuplem1  45517  smfsupmpt  45521  smfsupxr  45522  smfinflem  45523  smfinfmpt  45525  smflimsuplem5  45530  smflimsuplem7  45532  smflimsuplem8  45533  smflimsupmpt  45535  smfliminflem  45536  smfliminfmpt  45538  smfpimne2  45546  fsupdm  45548  smfsupdmmbllem  45550  finfdm  45552  smfinfdmmbllem  45554  or2expropbilem2  45733  or2expropbi  45734  cfsetsnfsetf  45758  2reu8i  45811  nfdfat  45825  iccelpart  46091  ichnfim  46122  ich2exprop  46129  ichreuopeq  46131  sprsymrelfo  46155  reupr  46180  reuopreuprim  46184  2zrngmmgm  46834  opeliun2xp  46998  cbvmpox2  47001  ovmpordxf  47004  1arymaptfo  47319  2arymaptfo  47330  setrec1  47726  pgindnf  47751  aacllem  47838