Theorem nfan 1900

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

Syntax hints:   ∧ wa 395  ⊤wtru 1542  Ⅎwnf 1784

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfnan  1901  nf3an  1902  hban  2304  nfeqf  2383  nfald2  2447  2ax6elem  2472  nfsb4t  2501  nfeu1ALT  2586  eupicka  2631  mopick2  2634  2mo  2645  nfabd2  2920  2ralbida  3257  r19.12  3283  reean  3284  ralcom2  3345  cbvrmow  3373  nfrmow  3377  nfreuw  3378  cbvreu  3389  cbvrabw  3432  cbvrabwOLD  3433  nfrabw  3434  cbvrab  3437  ceqsex2  3491  vtocl2gafOLD  3533  vtocl3gaf  3534  spc2ed  3553  rspce  3563  eqvincf  3602  elrabf  3641  elrab3t  3643  rexab2  3655  morex  3675  reu2  3681  rmo3f  3690  reu2eqd  3692  sbc2iegf  3813  reu8nf  3825  rmo2  3835  rmo3  3837  csbiebt  3876  csbie2t  3885  cbvrabcsfw  3888  cbvreucsf  3891  cbvrabcsf  3892  nfdif  4080  nfin  4175  reusngf  4628  rexreusng  4633  reuprg0  4656  rabsnifsb  4676  nfop  4842  nfopd  4843  eluniab  4874  iuneqconst  4955  cbvopab  5167  cbvopab1  5169  cbvopab1g  5170  cbvopab2  5171  cbvopab1s  5172  mpteq12f  5180  nfmpt  5193  cbvmptf  5195  cbvmptfg  5196  axrep3  5225  axrep4OLD  5228  axrep5  5229  reusv2lem3  5342  axprlem4OLD  5371  axprlem5OLD  5372  nfpo  5535  nfso  5536  nffr  5594  nfwe  5596  nfxp  5654  opeliunxp  5688  opeliun2xp  5689  nfco  5812  elrnmpt1  5907  nfimad  6025  reuop  6248  iota2  6478  nffun  6512  imadif  6573  nffn  6588  nff  6655  nff1  6725  nffo  6742  nff1o  6769  nffvd  6843  fv3  6849  funimassd  6897  fvmptdf  6944  fompt  7060  f1ossf1o  7070  fmptco  7071  fsnex  7226  nfiso  7265  nfriotadw  7320  cbvriotaw  7321  nfriotad  7323  cbvriota  7325  riota2df  7335  riota5f  7340  oprabv  7415  nfoprab  7419  mpoeq123  7427  nfmpo  7437  cbvoprab1  7442  cbvoprab2  7443  cbvoprab12  7444  cbvoprab3  7446  cbvmpox  7448  ovmpodxf  7505  elovmporab  7601  elovmporab1w  7602  elovmporab1  7603  onminex  7744  fiun  7884  f1iun  7885  opabex3d  7906  opabex3rd  7907  opabex3  7908  dfoprab4f  7997  fmpox  8008  opeliunxp2f  8149  nffrecs  8222  frrlem4  8228  tfr3  8327  tz7.49  8373  naddsuc2  8625  erovlem  8746  nfixpw  8849  nfixp  8850  nfixp1  8851  xpf1o  9062  nneneq  9125  ac6sfi  9178  nfoi  9410  wdom2d  9476  infpssrlem4  10207  hsmexlem2  10328  hsmexlem4  10330  domtriomlem  10343  axdc3lem2  10352  axdc4lem  10356  zorn2lem4  10400  zorn2lem5  10401  konigthlem  10469  axextnd  10492  axrepndlem2  10494  axrepnd  10495  axunnd  10497  axpowndlem2  10499  axpowndlem4  10501  axpownd  10502  axregndlem2  10504  axregnd  10505  axinfndlem1  10506  axinfnd  10507  zfcndrep  10515  zfcndinf  10519  dedekind  11286  dedekindle  11287  fsuppmapnn0fiublem  13907  fsuppmapnn0fiub  13908  fsuppmapnn0fiubex  13909  reuccatpfxs1  14664  nfsum1  15607  nfsum  15608  fsumclf  15655  fsumsplitf  15659  fsumsplit1  15662  fsum2dlem  15687  fsum00  15715  nfcprod1  15825  nfcprod  15826  fprod2dlem  15897  fprodsplitf  15905  fprodsplit1f  15907  fprodle  15913  lcmfunsnlem1  16558  lcmfunsnlem2lem1  16559  lcmfunsnlem2  16561  mreexexd  17564  acsmapd  18470  gsum2d2lem  19895  dprd2d2  19968  gsummoncoe1  22233  gsummatr01lem4  22583  cpmatmcllem  22643  cayleyhamilton1  22817  neiptopnei  23057  neiptopreu  23058  neitr  23105  iunconnlem  23352  iunconn  23353  ptcnplem  23546  ptcnp  23547  xkocnv  23739  isfildlem  23782  utopsnneiplem  24172  isucn2  24203  cfilucfil  24484  restmetu  24495  ovolfiniun  25439  ovoliunlem3  25442  ovoliunnul  25445  volfiniun  25485  itg2splitlem  25686  itg2split  25687  isibl2  25704  nfitg  25713  cbvitg  25714  limciun  25832  2sqmo  27385  2sqreulem4  27402  istrkg2ld  28448  chirred  32386  sbc2iedf  32455  rspc2daf  32456  opreu2reuALT  32467  mo5f  32479  foresf1o  32495  iinabrex  32560  cbvdisjf  32562  disjabrex  32573  disjabrexf  32574  funimass4f  32630  2ndresdju  32642  fmptcof2  32650  fcomptf  32651  acunirnmpt2  32653  acunirnmpt2f  32654  aciunf1lem  32655  funcnv4mpt  32662  fnpreimac  32664  f1od2  32713  fpwrelmap  32727  xrofsup  32761  nn0min  32814  fprodex01  32819  fsumiunle  32823  prodindf  32855  isarchiofld  33179  elrgspnsubrunlem2  33226  nsgqusf1olem1  33389  nsgqusf1olem3  33391  elrspunidl  33404  mplvrpmga  33586  fedgmullem2  33654  irngnzply1  33715  reff  33863  locfinreflem  33864  cmpcref  33874  zarclsiin  33895  zarcmplem  33905  ordtconnlem1  33948  esumcl  34054  gsumesum  34083  esumlub  34084  esumcst  34087  esumrnmpt2  34092  esumfzf  34093  esumfsup  34094  hasheuni  34109  esumcvg  34110  esumgect  34114  esumcvgre  34115  esum2dlem  34116  esum2d  34117  esumiun  34118  ldsysgenld  34184  sigapildsyslem  34185  sigapildsys  34186  ldgenpisyslem1  34187  measvunilem  34236  measvunilem0  34237  measvuni  34238  measinblem  34244  voliune  34253  volfiniune  34254  volmeas  34255  oms0  34321  omssubadd  34324  eulerpartlemgvv  34400  dstrvprob  34496  breprexplema  34654  bnj919  34790  bnj1146  34814  bnj1379  34853  bnj849  34948  bnj916  34956  bnj964  34966  bnj1014  34984  bnj1123  35009  bnj1228  35034  bnj1307  35046  bnj1321  35050  bnj1398  35057  bnj1408  35059  bnj1444  35066  bnj1445  35067  bnj1446  35068  bnj1449  35071  bnj1467  35077  bnj1463  35078  bnj1489  35079  bnj1491  35080  bnj1312  35081  bnj1525  35092  dvelimalcased  35098  dvelimexcased  35100  fineqvrep  35148  cvmcov  35318  iota5f  35779  axextdist  35852  axextbdist  35853  nfwlim  35875  finminlem  36373  bj-dvelimdv  36906  bj-opabco  37243  isbasisrelowllem1  37410  isbasisrelowllem2  37411  fvineqsneu  37466  fvineqsneq  37467  wl-cbvalnaed  37587  wl-2sb6d  37613  wl-sbalnae  37617  wl-mo2tf  37626  wl-eutf  37628  phpreu  37654  poimirlem26  37696  poimirlem27  37697  heicant  37705  mbfposadd  37717  ftc1anclem5  37747  indexdom  37784  filbcmb  37790  sdclem2  37792  sdclem1  37793  fdc1  37796  riotasv2d  39066  riotasv2s  39067  nfded2  39077  glbconxN  39487  pmapglb2xN  39881  cdlemefs32sn1aw  40523  mzpsubmpt  42850  mzpexpmpt  42852  eq0rabdioph  42883  eqrabdioph  42884  setindtr  43131  unielss  43325  nadd1suc  43499  ss2iundf  43766  scottabf  44347  mnuprdlem4  44382  ismnushort  44408  binomcxplemnotnn0  44463  iunconnlem2  45041  nfrelp  45056  modelaxreplem3  45087  modelaxrep  45088  permaxrep  45113  elunif  45127  rspcegf  45134  fnchoice  45140  refsumcn  45141  rfcnnnub  45147  uzwo4  45164  fiiuncl  45176  cbvmpo2  45208  cbvmpo1  45209  iinssiin  45240  disjf1  45294  disjrnmpt2  45299  disjf1o  45302  disjinfi  45303  choicefi  45311  axccdom  45333  dmrelrnrel  45337  axccd  45340  rnmptbddlem  45355  rnmptbd2lem  45359  infnsuprnmpt  45361  rnmptbdlem  45366  rnmptssbi  45371  upbdrech  45420  ssfiunibd  45424  supxrgere  45446  supxrgelem  45450  supxrge  45451  xralrple2  45467  infxr  45479  infxrunb2  45480  xrralrecnnle  45495  xrralrecnnge  45502  supxrunb3  45511  supxrleubrnmpt  45518  infleinf2  45526  unb2ltle  45527  rexabslelem  45530  suprleubrnmpt  45534  uzub  45543  supminfrnmpt  45557  supxrleubrnmptf  45563  infxrgelbrnmpt  45566  infrpgernmpt  45577  monoordxr  45594  monoord2xr  45596  caucvgbf  45601  cvgcaule  45603  iccshift  45632  iooshift  45636  iooiinicc  45656  iooiinioc  45670  fsummulc1f  45685  fsumf1of  45688  fsumreclf  45690  fsumlessf  45691  fmul01  45694  fmuldfeqlem1  45696  fmuldfeq  45697  fmul01lt1lem1  45698  fmul01lt1lem2  45699  fprodexp  45708  mccl  45712  fprodcnlem  45713  fprodcn  45714  climmulf  45718  climexp  45719  climsuse  45722  climrecf  45723  climinff  45725  climaddf  45729  mullimc  45730  islptre  45733  climf  45736  mullimcf  45737  rexlim2d  45739  idlimc  45740  limcperiod  45742  limcrecl  45743  islpcn  45751  limsupre  45753  limcleqr  45756  addlimc  45760  limclner  45763  climsubmpt  45772  climreclf  45776  climf2  45778  climeldmeqmpt  45780  clim2f2  45782  climfveqmpt  45783  fnlimfvre  45786  allbutfifvre  45787  climleltrp  45788  fnlimf  45790  fnlimabslt  45791  climfveqf  45792  climfveqmpt3  45794  climeldmeqf  45795  climeqf  45800  climeldmeqmpt3  45801  limsuppnfd  45814  limsupub  45816  climinf2lem  45818  climinf2  45819  limsuppnf  45823  limsupubuz  45825  climinf2mpt  45826  climinfmpt  45827  climinf3  45828  limsupmnflem  45832  limsupequz  45835  limsupre2  45837  limsupmnfuzlem  45838  limsupequzmptf  45843  limsupre3  45845  limsupre3uzlem  45847  limsupreuzmpt  45851  climisp  45858  lmbr3  45859  climrescn  45860  climxrrelem  45861  climxrre  45862  limsupub2  45924  liminflbuz2  45927  xlimmnfvlem2  45945  xlimmnfv  45946  xlimpnfvlem2  45949  xlimpnfv  45950  xlimmnfmpt  45955  xlimpnfmpt  45956  climxlim2lem  45957  cncficcgt0  46000  cncfioobd  46009  fprodsubrecnncnvlem  46019  fprodaddrecnncnvlem  46021  dvmptmulf  46049  dvnmul  46055  dvmptfprodlem  46056  dvmptfprod  46057  dvnprodlem1  46058  dvnprodlem2  46059  iblsplitf  46082  itgperiod  46093  stoweidlem3  46115  stoweidlem26  46138  stoweidlem27  46139  stoweidlem29  46141  stoweidlem31  46143  stoweidlem34  46146  stoweidlem35  46147  stoweidlem36  46148  stoweidlem39  46151  stoweidlem42  46154  stoweidlem43  46155  stoweidlem44  46156  stoweidlem46  46158  stoweidlem48  46160  stoweidlem49  46161  stoweidlem51  46163  stoweidlem52  46164  stoweidlem53  46165  stoweidlem54  46166  stoweidlem55  46167  stoweidlem56  46168  stoweidlem57  46169  stoweidlem58  46170  stoweidlem59  46171  stoweidlem60  46172  stoweidlem61  46173  stoweidlem62  46174  stoweid  46175  wallispilem3  46179  stirlinglem13  46198  stirling  46201  fourierdlem16  46235  fourierdlem21  46240  fourierdlem22  46241  fourierdlem31  46250  fourierdlem39  46258  fourierdlem48  46266  fourierdlem51  46269  fourierdlem68  46286  fourierdlem71  46289  fourierdlem73  46291  fourierdlem80  46298  fourierdlem81  46299  fourierdlem86  46304  fourierdlem87  46305  fourierdlem93  46311  fourierdlem94  46312  fourierdlem103  46321  fourierdlem104  46322  fourierdlem112  46330  fourierdlem113  46331  elaa2  46346  etransclem32  46378  salexct  46446  sge0revalmpt  46490  sge0f1o  46494  sge0lefi  46510  sge0resplit  46518  sge0lempt  46522  sge0iunmptlemre  46527  sge0fodjrnlem  46528  sge0iunmpt  46530  sge0ltfirpmpt2  46538  sge0isum  46539  sge0xp  46541  sge0isummpt2  46544  sge0xadd  46547  sge0pnffsumgt  46554  sge0gtfsumgt  46555  sge0uzfsumgt  46556  sge0reuz  46559  sge0reuzb  46560  iundjiun  46572  meadjiun  46578  ismeannd  46579  voliunsge0lem  46584  meaiunincf  46595  meaiuninc3v  46596  meaiuninc3  46597  meaiininc  46599  caragenfiiuncl  46627  omeiunltfirp  46631  ovnsubaddlem2  46683  hoidmvval0  46699  hoidmvlelem1  46707  hoidmvlelem3  46709  hoidmvlelem5  46711  ovnlecvr2  46722  hspdifhsp  46728  hoiqssbllem2  46735  hoiqssbllem3  46736  hspmbllem2  46739  opnvonmbllem2  46745  hoimbl2  46777  vonhoire  46784  iinhoiicc  46786  iunhoiioolem  46787  iunhoiioo  46788  vonioo  46794  vonicc  46797  vonn0ioo2  46802  vonn0icc2  46804  salpreimagelt  46819  salpreimalegt  46821  pimincfltioc  46828  pimdecfgtioo  46829  pimincfltioo  46830  preimageiingt  46832  preimaleiinlt  46833  salpreimagtge  46837  salpreimaltle  46838  salpreimalelt  46841  salpreimagtlt  46842  incsmflem  46853  issmflelem  46856  issmfle  46857  smfconst  46861  issmfgtlem  46867  issmfgt  46868  smfaddlem2  46876  smfadd  46877  decsmflem  46878  decsmf  46879  issmfgelem  46881  issmfge  46882  smflimlem2  46884  smflim  46889  smfresal  46900  smfrec  46901  smfmullem4  46906  smfmul  46907  smfpimcc  46920  smflimmpt  46922  smfsuplem1  46923  smfsupmpt  46927  smfsupxr  46928  smfinflem  46929  smfinfmpt  46931  smflimsuplem5  46936  smflimsuplem7  46938  smflimsuplem8  46939  smflimsupmpt  46941  smfliminflem  46942  smfliminfmpt  46944  smfpimne2  46952  fsupdm  46954  smfsupdmmbllem  46956  finfdm  46958  smfinfdmmbllem  46960  or2expropbilem2  47147  or2expropbi  47148  cfsetsnfsetf  47172  2reu8i  47227  nfdfat  47241  iccelpart  47547  ichnfim  47578  ich2exprop  47585  ichreuopeq  47587  sprsymrelfo  47611  reupr  47636  reuopreuprim  47640  2zrngmmgm  48366  cbvmpox2  48450  ovmpordxf  48453  1arymaptfo  48758  2arymaptfo  48769  iinfssclem3  49171  iinfssc  49172  iinfsubc  49173  setrec1  49806  pgindnf  49831  aacllem  49916