Theorem nfan 1899

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

Syntax hints:   ∧ wa 395  ⊤wtru 1541  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfnan  1900  nf3an  1901  hban  2300  nfeqf  2379  nfald2  2443  2ax6elem  2468  nfsb4t  2497  nfeu1ALT  2582  eupicka  2627  mopick2  2630  2mo  2641  nfabd2  2915  2ralbida  3260  r19.12  3288  reean  3289  ralcom2  3351  cbvrmow  3381  nfrmow  3385  nfreuw  3386  cbvreu  3397  cbvrabw  3441  cbvrabwOLD  3442  nfrabw  3443  cbvrab  3446  ceqsex2  3501  vtocl2gafOLD  3546  vtocl3gaf  3547  spc2ed  3567  rspce  3577  eqvincf  3616  elrabf  3655  elrab3t  3658  rexab2  3670  morex  3690  reu2  3696  rmo3f  3705  reu2eqd  3707  sbc2iegf  3828  reu8nf  3840  rmo2  3850  rmo3  3852  csbiebt  3891  csbie2t  3900  cbvrabcsfw  3903  cbvreucsf  3906  cbvrabcsf  3907  nfdif  4092  nfin  4187  reusngf  4638  rexreusng  4643  reuprg0  4666  rabsnifsb  4686  nfop  4853  nfopd  4854  eluniab  4885  iuneqconst  4967  cbvopab  5179  cbvopab1  5181  cbvopab1g  5182  cbvopab2  5183  cbvopab1s  5184  mpteq12f  5192  nfmpt  5205  cbvmptf  5207  cbvmptfg  5208  axrep3  5238  axrep4OLD  5241  axrep5  5242  reusv2lem3  5355  axprlem4OLD  5384  axprlem5OLD  5385  nfpo  5552  nfso  5553  nffr  5611  nfwe  5613  nfxp  5671  opeliunxp  5705  opeliun2xp  5706  nfco  5829  elrnmpt1  5924  nfimad  6040  reuop  6266  iota2  6500  nffun  6539  imadif  6600  nffn  6617  nff  6684  nff1  6754  nffo  6771  nff1o  6798  nffvd  6870  fv3  6876  funimassd  6927  fvmptdf  6974  fompt  7090  f1ossf1o  7100  fmptco  7101  fsnex  7258  nfiso  7297  nfriotadw  7352  cbvriotaw  7353  nfriotad  7355  cbvriota  7357  riota2df  7367  riota5f  7372  oprabv  7449  nfoprab  7453  mpoeq123  7461  nfmpo  7471  cbvoprab1  7476  cbvoprab2  7477  cbvoprab12  7478  cbvoprab3  7480  cbvmpox  7482  ovmpodxf  7539  elovmporab  7635  elovmporab1w  7636  elovmporab1  7637  onminex  7778  fiun  7921  f1iun  7922  opabex3d  7944  opabex3rd  7945  opabex3  7946  dfoprab4f  8035  fmpox  8046  opeliunxp2f  8189  nffrecs  8262  frrlem4  8268  tfr3  8367  tz7.49  8413  naddsuc2  8665  erovlem  8786  nfixpw  8889  nfixp  8890  nfixp1  8891  xpf1o  9103  nneneq  9170  ac6sfi  9231  nfoi  9467  wdom2d  9533  infpssrlem4  10259  hsmexlem2  10380  hsmexlem4  10382  domtriomlem  10395  axdc3lem2  10404  axdc4lem  10408  zorn2lem4  10452  zorn2lem5  10453  konigthlem  10521  axextnd  10544  axrepndlem2  10546  axrepnd  10547  axunnd  10549  axpowndlem2  10551  axpowndlem4  10553  axpownd  10554  axregndlem2  10556  axregnd  10557  axinfndlem1  10558  axinfnd  10559  zfcndrep  10567  zfcndinf  10571  dedekind  11337  dedekindle  11338  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  fsuppmapnn0fiubex  13957  reuccatpfxs1  14712  nfsum1  15656  nfsum  15657  fsumclf  15704  fsumsplitf  15708  fsumsplit1  15711  fsum2dlem  15736  fsum00  15764  nfcprod1  15874  nfcprod  15875  fprod2dlem  15946  fprodsplitf  15954  fprodsplit1f  15956  fprodle  15962  lcmfunsnlem1  16607  lcmfunsnlem2lem1  16608  lcmfunsnlem2  16610  mreexexd  17609  acsmapd  18513  gsum2d2lem  19903  dprd2d2  19976  gsummoncoe1  22195  gsummatr01lem4  22545  cpmatmcllem  22605  cayleyhamilton1  22779  neiptopnei  23019  neiptopreu  23020  neitr  23067  iunconnlem  23314  iunconn  23315  ptcnplem  23508  ptcnp  23509  xkocnv  23701  isfildlem  23744  utopsnneiplem  24135  isucn2  24166  cfilucfil  24447  restmetu  24458  ovolfiniun  25402  ovoliunlem3  25405  ovoliunnul  25408  volfiniun  25448  itg2splitlem  25649  itg2split  25650  isibl2  25667  nfitg  25676  cbvitg  25677  limciun  25795  2sqmo  27348  2sqreulem4  27365  istrkg2ld  28387  chirred  32324  sbc2iedf  32394  rspc2daf  32395  opreu2reuALT  32406  mo5f  32418  foresf1o  32433  iinabrex  32498  cbvdisjf  32500  disjabrex  32511  disjabrexf  32512  funimass4f  32561  2ndresdju  32573  fmptcof2  32581  fcomptf  32582  acunirnmpt2  32584  acunirnmpt2f  32585  aciunf1lem  32586  funcnv4mpt  32593  fnpreimac  32595  f1od2  32644  fpwrelmap  32656  xrofsup  32690  nn0min  32745  fprodex01  32750  fsumiunle  32754  prodindf  32786  elrgspnsubrunlem2  33199  isarchiofld  33295  nsgqusf1olem1  33384  nsgqusf1olem3  33386  elrspunidl  33399  fedgmullem2  33626  irngnzply1  33686  reff  33829  locfinreflem  33830  cmpcref  33840  zarclsiin  33861  zarcmplem  33871  ordtconnlem1  33914  esumcl  34020  gsumesum  34049  esumlub  34050  esumcst  34053  esumrnmpt2  34058  esumfzf  34059  esumfsup  34060  hasheuni  34075  esumcvg  34076  esumgect  34080  esumcvgre  34081  esum2dlem  34082  esum2d  34083  esumiun  34084  ldsysgenld  34150  sigapildsyslem  34151  sigapildsys  34152  ldgenpisyslem1  34153  measvunilem  34202  measvunilem0  34203  measvuni  34204  measinblem  34210  voliune  34219  volfiniune  34220  volmeas  34221  oms0  34288  omssubadd  34291  eulerpartlemgvv  34367  dstrvprob  34463  breprexplema  34621  bnj919  34757  bnj1146  34781  bnj1379  34820  bnj849  34915  bnj916  34923  bnj964  34933  bnj1014  34951  bnj1123  34976  bnj1228  35001  bnj1307  35013  bnj1321  35017  bnj1398  35024  bnj1408  35026  bnj1444  35033  bnj1445  35034  bnj1446  35035  bnj1449  35038  bnj1467  35044  bnj1463  35045  bnj1489  35046  bnj1491  35047  bnj1312  35048  bnj1525  35059  dvelimalcased  35065  dvelimexcased  35067  fineqvrep  35085  cvmcov  35250  iota5f  35711  axextdist  35787  axextbdist  35788  nfwlim  35810  finminlem  36306  bj-dvelimdv  36839  bj-opabco  37176  isbasisrelowllem1  37343  isbasisrelowllem2  37344  fvineqsneu  37399  fvineqsneq  37400  wl-cbvalnaed  37520  wl-2sb6d  37546  wl-sbalnae  37550  wl-mo2tf  37559  wl-eutf  37561  wl-ax11-lem3  37575  phpreu  37598  poimirlem26  37640  poimirlem27  37641  heicant  37649  mbfposadd  37661  ftc1anclem5  37691  indexdom  37728  filbcmb  37734  sdclem2  37736  sdclem1  37737  fdc1  37740  riotasv2d  38950  riotasv2s  38951  nfded2  38961  glbconxN  39372  pmapglb2xN  39766  cdlemefs32sn1aw  40408  mzpsubmpt  42731  mzpexpmpt  42733  eq0rabdioph  42764  eqrabdioph  42765  setindtr  43013  unielss  43207  nadd1suc  43381  ss2iundf  43648  scottabf  44229  mnuprdlem4  44264  ismnushort  44290  binomcxplemnotnn0  44345  iunconnlem2  44924  nfrelp  44939  modelaxreplem3  44970  modelaxrep  44971  permaxrep  44996  elunif  45010  rspcegf  45017  fnchoice  45023  refsumcn  45024  rfcnnnub  45030  uzwo4  45047  fiiuncl  45059  cbvmpo2  45091  cbvmpo1  45092  iinssiin  45123  disjf1  45177  disjrnmpt2  45182  disjf1o  45185  disjinfi  45186  choicefi  45194  axccdom  45216  dmrelrnrel  45220  axccd  45223  rnmptbddlem  45238  rnmptbd2lem  45242  infnsuprnmpt  45244  rnmptbdlem  45249  rnmptssbi  45254  upbdrech  45303  ssfiunibd  45307  supxrgere  45329  supxrgelem  45333  supxrge  45334  xralrple2  45350  infxr  45363  infxrunb2  45364  xrralrecnnle  45379  xrralrecnnge  45386  supxrunb3  45395  supxrleubrnmpt  45402  infleinf2  45410  unb2ltle  45411  rexabslelem  45414  suprleubrnmpt  45418  uzub  45427  supminfrnmpt  45441  supxrleubrnmptf  45447  infxrgelbrnmpt  45450  infrpgernmpt  45461  monoordxr  45478  monoord2xr  45480  caucvgbf  45485  cvgcaule  45487  iccshift  45516  iooshift  45520  iooiinicc  45540  iooiinioc  45554  fsummulc1f  45569  fsumf1of  45572  fsumreclf  45574  fsumlessf  45575  fmul01  45578  fmuldfeqlem1  45580  fmuldfeq  45581  fmul01lt1lem1  45582  fmul01lt1lem2  45583  fprodexp  45592  mccl  45596  fprodcnlem  45597  fprodcn  45598  climmulf  45602  climexp  45603  climsuse  45606  climrecf  45607  climinff  45609  climaddf  45613  mullimc  45614  islptre  45617  climf  45620  mullimcf  45621  rexlim2d  45623  idlimc  45624  limcperiod  45626  limcrecl  45627  islpcn  45637  limsupre  45639  limcleqr  45642  addlimc  45646  limclner  45649  climsubmpt  45658  climreclf  45662  climf2  45664  climeldmeqmpt  45666  clim2f2  45668  climfveqmpt  45669  fnlimfvre  45672  allbutfifvre  45673  climleltrp  45674  fnlimf  45676  fnlimabslt  45677  climfveqf  45678  climfveqmpt3  45680  climeldmeqf  45681  climeqf  45686  climeldmeqmpt3  45687  limsuppnfd  45700  limsupub  45702  climinf2lem  45704  climinf2  45705  limsuppnf  45709  limsupubuz  45711  climinf2mpt  45712  climinfmpt  45713  climinf3  45714  limsupmnflem  45718  limsupequz  45721  limsupre2  45723  limsupmnfuzlem  45724  limsupequzmptf  45729  limsupre3  45731  limsupre3uzlem  45733  limsupreuzmpt  45737  climisp  45744  lmbr3  45745  climrescn  45746  climxrrelem  45747  climxrre  45748  limsupub2  45810  liminflbuz2  45813  xlimmnfvlem2  45831  xlimmnfv  45832  xlimpnfvlem2  45835  xlimpnfv  45836  xlimmnfmpt  45841  xlimpnfmpt  45842  climxlim2lem  45843  cncficcgt0  45886  cncfioobd  45895  fprodsubrecnncnvlem  45905  fprodaddrecnncnvlem  45907  dvmptmulf  45935  dvnmul  45941  dvmptfprodlem  45942  dvmptfprod  45943  dvnprodlem1  45944  dvnprodlem2  45945  iblsplitf  45968  itgperiod  45979  stoweidlem3  46001  stoweidlem26  46024  stoweidlem27  46025  stoweidlem29  46027  stoweidlem31  46029  stoweidlem34  46032  stoweidlem35  46033  stoweidlem36  46034  stoweidlem39  46037  stoweidlem42  46040  stoweidlem43  46041  stoweidlem44  46042  stoweidlem46  46044  stoweidlem48  46046  stoweidlem49  46047  stoweidlem51  46049  stoweidlem52  46050  stoweidlem53  46051  stoweidlem54  46052  stoweidlem55  46053  stoweidlem56  46054  stoweidlem57  46055  stoweidlem58  46056  stoweidlem59  46057  stoweidlem60  46058  stoweidlem61  46059  stoweidlem62  46060  stoweid  46061  wallispilem3  46065  stirlinglem13  46084  stirling  46087  fourierdlem16  46121  fourierdlem21  46126  fourierdlem22  46127  fourierdlem31  46136  fourierdlem39  46144  fourierdlem48  46152  fourierdlem51  46155  fourierdlem68  46172  fourierdlem71  46175  fourierdlem73  46177  fourierdlem80  46184  fourierdlem81  46185  fourierdlem86  46190  fourierdlem87  46191  fourierdlem93  46197  fourierdlem94  46198  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  fourierdlem113  46217  elaa2  46232  etransclem32  46264  salexct  46332  sge0revalmpt  46376  sge0f1o  46380  sge0lefi  46396  sge0resplit  46404  sge0lempt  46408  sge0iunmptlemre  46413  sge0fodjrnlem  46414  sge0iunmpt  46416  sge0ltfirpmpt2  46424  sge0isum  46425  sge0xp  46427  sge0isummpt2  46430  sge0xadd  46433  sge0pnffsumgt  46440  sge0gtfsumgt  46441  sge0uzfsumgt  46442  sge0reuz  46445  sge0reuzb  46446  iundjiun  46458  meadjiun  46464  ismeannd  46465  voliunsge0lem  46470  meaiunincf  46481  meaiuninc3v  46482  meaiuninc3  46483  meaiininc  46485  caragenfiiuncl  46513  omeiunltfirp  46517  ovnsubaddlem2  46569  hoidmvval0  46585  hoidmvlelem1  46593  hoidmvlelem3  46595  hoidmvlelem5  46597  ovnlecvr2  46608  hspdifhsp  46614  hoiqssbllem2  46621  hoiqssbllem3  46622  hspmbllem2  46625  opnvonmbllem2  46631  hoimbl2  46663  vonhoire  46670  iinhoiicc  46672  iunhoiioolem  46673  iunhoiioo  46674  vonioo  46680  vonicc  46683  vonn0ioo2  46688  vonn0icc2  46690  salpreimagelt  46705  salpreimalegt  46707  pimincfltioc  46714  pimdecfgtioo  46715  pimincfltioo  46716  preimageiingt  46718  preimaleiinlt  46719  salpreimagtge  46723  salpreimaltle  46724  salpreimalelt  46727  salpreimagtlt  46728  incsmflem  46739  issmflelem  46742  issmfle  46743  smfconst  46747  issmfgtlem  46753  issmfgt  46754  smfaddlem2  46762  smfadd  46763  decsmflem  46764  decsmf  46765  issmfgelem  46767  issmfge  46768  smflimlem2  46770  smflim  46775  smfresal  46786  smfrec  46787  smfmullem4  46792  smfmul  46793  smfpimcc  46806  smflimmpt  46808  smfsuplem1  46809  smfsupmpt  46813  smfsupxr  46814  smfinflem  46815  smfinfmpt  46817  smflimsuplem5  46822  smflimsuplem7  46824  smflimsuplem8  46825  smflimsupmpt  46827  smfliminflem  46828  smfliminfmpt  46830  smfpimne2  46838  fsupdm  46840  smfsupdmmbllem  46842  finfdm  46844  smfinfdmmbllem  46846  or2expropbilem2  47034  or2expropbi  47035  cfsetsnfsetf  47059  2reu8i  47114  nfdfat  47128  iccelpart  47434  ichnfim  47465  ich2exprop  47472  ichreuopeq  47474  sprsymrelfo  47498  reupr  47523  reuopreuprim  47527  2zrngmmgm  48240  cbvmpox2  48324  ovmpordxf  48327  1arymaptfo  48632  2arymaptfo  48643  iinfssclem3  49045  iinfssc  49046  iinfsubc  49047  setrec1  49680  pgindnf  49705  aacllem  49790