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  2302  nfeqf  2381  nfald2  2445  2ax6elem  2470  nfsb4t  2499  nfeu1ALT  2584  eupicka  2629  mopick2  2632  2mo  2643  nfabd2  2918  2ralbida  3255  r19.12  3281  reean  3282  ralcom2  3343  cbvrmow  3371  nfrmow  3375  nfreuw  3376  cbvreu  3387  cbvrabw  3430  cbvrabwOLD  3431  nfrabw  3432  cbvrab  3435  ceqsex2  3489  vtocl2gafOLD  3531  vtocl3gaf  3532  spc2ed  3551  rspce  3561  eqvincf  3600  elrabf  3639  elrab3t  3641  rexab2  3653  morex  3673  reu2  3679  rmo3f  3688  reu2eqd  3690  sbc2iegf  3811  reu8nf  3823  rmo2  3833  rmo3  3835  csbiebt  3874  csbie2t  3883  cbvrabcsfw  3886  cbvreucsf  3889  cbvrabcsf  3890  nfdif  4076  nfin  4171  reusngf  4624  rexreusng  4629  reuprg0  4652  rabsnifsb  4672  nfop  4838  nfopd  4839  eluniab  4870  iuneqconst  4951  cbvopab  5161  cbvopab1  5163  cbvopab1g  5164  cbvopab2  5165  cbvopab1s  5166  mpteq12f  5174  nfmpt  5187  cbvmptf  5189  cbvmptfg  5190  axrep3  5219  axrep4OLD  5222  axrep5  5223  reusv2lem3  5336  axprlem4OLD  5365  axprlem5OLD  5366  nfpo  5528  nfso  5529  nffr  5587  nfwe  5589  nfxp  5647  opeliunxp  5681  opeliun2xp  5682  nfco  5804  elrnmpt1  5899  nfimad  6017  reuop  6240  iota2  6470  nffun  6504  imadif  6565  nffn  6580  nff  6647  nff1  6717  nffo  6734  nff1o  6761  nffvd  6834  fv3  6840  funimassd  6888  fvmptdf  6935  fompt  7051  f1ossf1o  7061  fmptco  7062  fsnex  7217  nfiso  7256  nfriotadw  7311  cbvriotaw  7312  nfriotad  7314  cbvriota  7316  riota2df  7326  riota5f  7331  oprabv  7406  nfoprab  7410  mpoeq123  7418  nfmpo  7428  cbvoprab1  7433  cbvoprab2  7434  cbvoprab12  7435  cbvoprab3  7437  cbvmpox  7439  ovmpodxf  7496  elovmporab  7592  elovmporab1w  7593  elovmporab1  7594  onminex  7735  fiun  7875  f1iun  7876  opabex3d  7897  opabex3rd  7898  opabex3  7899  dfoprab4f  7988  fmpox  7999  opeliunxp2f  8140  nffrecs  8213  frrlem4  8219  tfr3  8318  tz7.49  8364  naddsuc2  8616  erovlem  8737  nfixpw  8840  nfixp  8841  nfixp1  8842  xpf1o  9052  nneneq  9115  ac6sfi  9168  nfoi  9400  wdom2d  9466  infpssrlem4  10197  hsmexlem2  10318  hsmexlem4  10320  domtriomlem  10333  axdc3lem2  10342  axdc4lem  10346  zorn2lem4  10390  zorn2lem5  10391  konigthlem  10459  axextnd  10482  axrepndlem2  10484  axrepnd  10485  axunnd  10487  axpowndlem2  10489  axpowndlem4  10491  axpownd  10492  axregndlem2  10494  axregnd  10495  axinfndlem1  10496  axinfnd  10497  zfcndrep  10505  zfcndinf  10509  dedekind  11276  dedekindle  11277  fsuppmapnn0fiublem  13897  fsuppmapnn0fiub  13898  fsuppmapnn0fiubex  13899  reuccatpfxs1  14654  nfsum1  15597  nfsum  15598  fsumclf  15645  fsumsplitf  15649  fsumsplit1  15652  fsum2dlem  15677  fsum00  15705  nfcprod1  15815  nfcprod  15816  fprod2dlem  15887  fprodsplitf  15895  fprodsplit1f  15897  fprodle  15903  lcmfunsnlem1  16548  lcmfunsnlem2lem1  16549  lcmfunsnlem2  16551  mreexexd  17554  acsmapd  18460  gsum2d2lem  19885  dprd2d2  19958  gsummoncoe1  22223  gsummatr01lem4  22573  cpmatmcllem  22633  cayleyhamilton1  22807  neiptopnei  23047  neiptopreu  23048  neitr  23095  iunconnlem  23342  iunconn  23343  ptcnplem  23536  ptcnp  23537  xkocnv  23729  isfildlem  23772  utopsnneiplem  24162  isucn2  24193  cfilucfil  24474  restmetu  24485  ovolfiniun  25429  ovoliunlem3  25432  ovoliunnul  25435  volfiniun  25475  itg2splitlem  25676  itg2split  25677  isibl2  25694  nfitg  25703  cbvitg  25704  limciun  25822  2sqmo  27375  2sqreulem4  27392  istrkg2ld  28438  chirred  32375  sbc2iedf  32444  rspc2daf  32445  opreu2reuALT  32456  mo5f  32468  foresf1o  32484  iinabrex  32549  cbvdisjf  32551  disjabrex  32562  disjabrexf  32563  funimass4f  32619  2ndresdju  32631  fmptcof2  32639  fcomptf  32640  acunirnmpt2  32642  acunirnmpt2f  32643  aciunf1lem  32644  funcnv4mpt  32651  fnpreimac  32653  f1od2  32702  fpwrelmap  32716  xrofsup  32750  nn0min  32803  fprodex01  32808  fsumiunle  32812  prodindf  32844  isarchiofld  33168  elrgspnsubrunlem2  33215  nsgqusf1olem1  33378  nsgqusf1olem3  33380  elrspunidl  33393  mplvrpmga  33575  fedgmullem2  33643  irngnzply1  33704  reff  33852  locfinreflem  33853  cmpcref  33863  zarclsiin  33884  zarcmplem  33894  ordtconnlem1  33937  esumcl  34043  gsumesum  34072  esumlub  34073  esumcst  34076  esumrnmpt2  34081  esumfzf  34082  esumfsup  34083  hasheuni  34098  esumcvg  34099  esumgect  34103  esumcvgre  34104  esum2dlem  34105  esum2d  34106  esumiun  34107  ldsysgenld  34173  sigapildsyslem  34174  sigapildsys  34175  ldgenpisyslem1  34176  measvunilem  34225  measvunilem0  34226  measvuni  34227  measinblem  34233  voliune  34242  volfiniune  34243  volmeas  34244  oms0  34310  omssubadd  34313  eulerpartlemgvv  34389  dstrvprob  34485  breprexplema  34643  bnj919  34779  bnj1146  34803  bnj1379  34842  bnj849  34937  bnj916  34945  bnj964  34955  bnj1014  34973  bnj1123  34998  bnj1228  35023  bnj1307  35035  bnj1321  35039  bnj1398  35046  bnj1408  35048  bnj1444  35055  bnj1445  35056  bnj1446  35057  bnj1449  35060  bnj1467  35066  bnj1463  35067  bnj1489  35068  bnj1491  35069  bnj1312  35070  bnj1525  35081  dvelimalcased  35087  dvelimexcased  35089  fineqvrep  35137  cvmcov  35307  iota5f  35768  axextdist  35841  axextbdist  35842  nfwlim  35864  finminlem  36362  bj-dvelimdv  36895  bj-opabco  37232  isbasisrelowllem1  37399  isbasisrelowllem2  37400  fvineqsneu  37455  fvineqsneq  37456  wl-cbvalnaed  37576  wl-2sb6d  37602  wl-sbalnae  37606  wl-mo2tf  37615  wl-eutf  37617  phpreu  37643  poimirlem26  37685  poimirlem27  37686  heicant  37694  mbfposadd  37706  ftc1anclem5  37736  indexdom  37773  filbcmb  37779  sdclem2  37781  sdclem1  37782  fdc1  37785  riotasv2d  39055  riotasv2s  39056  nfded2  39066  glbconxN  39476  pmapglb2xN  39870  cdlemefs32sn1aw  40512  mzpsubmpt  42835  mzpexpmpt  42837  eq0rabdioph  42868  eqrabdioph  42869  setindtr  43116  unielss  43310  nadd1suc  43484  ss2iundf  43751  scottabf  44332  mnuprdlem4  44367  ismnushort  44393  binomcxplemnotnn0  44448  iunconnlem2  45026  nfrelp  45041  modelaxreplem3  45072  modelaxrep  45073  permaxrep  45098  elunif  45112  rspcegf  45119  fnchoice  45125  refsumcn  45126  rfcnnnub  45132  uzwo4  45149  fiiuncl  45161  cbvmpo2  45193  cbvmpo1  45194  iinssiin  45225  disjf1  45279  disjrnmpt2  45284  disjf1o  45287  disjinfi  45288  choicefi  45296  axccdom  45318  dmrelrnrel  45322  axccd  45325  rnmptbddlem  45340  rnmptbd2lem  45344  infnsuprnmpt  45346  rnmptbdlem  45351  rnmptssbi  45356  upbdrech  45405  ssfiunibd  45409  supxrgere  45431  supxrgelem  45435  supxrge  45436  xralrple2  45452  infxr  45464  infxrunb2  45465  xrralrecnnle  45480  xrralrecnnge  45487  supxrunb3  45496  supxrleubrnmpt  45503  infleinf2  45511  unb2ltle  45512  rexabslelem  45515  suprleubrnmpt  45519  uzub  45528  supminfrnmpt  45542  supxrleubrnmptf  45548  infxrgelbrnmpt  45551  infrpgernmpt  45562  monoordxr  45579  monoord2xr  45581  caucvgbf  45586  cvgcaule  45588  iccshift  45617  iooshift  45621  iooiinicc  45641  iooiinioc  45655  fsummulc1f  45670  fsumf1of  45673  fsumreclf  45675  fsumlessf  45676  fmul01  45679  fmuldfeqlem1  45681  fmuldfeq  45682  fmul01lt1lem1  45683  fmul01lt1lem2  45684  fprodexp  45693  mccl  45697  fprodcnlem  45698  fprodcn  45699  climmulf  45703  climexp  45704  climsuse  45707  climrecf  45708  climinff  45710  climaddf  45714  mullimc  45715  islptre  45718  climf  45721  mullimcf  45722  rexlim2d  45724  idlimc  45725  limcperiod  45727  limcrecl  45728  islpcn  45736  limsupre  45738  limcleqr  45741  addlimc  45745  limclner  45748  climsubmpt  45757  climreclf  45761  climf2  45763  climeldmeqmpt  45765  clim2f2  45767  climfveqmpt  45768  fnlimfvre  45771  allbutfifvre  45772  climleltrp  45773  fnlimf  45775  fnlimabslt  45776  climfveqf  45777  climfveqmpt3  45779  climeldmeqf  45780  climeqf  45785  climeldmeqmpt3  45786  limsuppnfd  45799  limsupub  45801  climinf2lem  45803  climinf2  45804  limsuppnf  45808  limsupubuz  45810  climinf2mpt  45811  climinfmpt  45812  climinf3  45813  limsupmnflem  45817  limsupequz  45820  limsupre2  45822  limsupmnfuzlem  45823  limsupequzmptf  45828  limsupre3  45830  limsupre3uzlem  45832  limsupreuzmpt  45836  climisp  45843  lmbr3  45844  climrescn  45845  climxrrelem  45846  climxrre  45847  limsupub2  45909  liminflbuz2  45912  xlimmnfvlem2  45930  xlimmnfv  45931  xlimpnfvlem2  45934  xlimpnfv  45935  xlimmnfmpt  45940  xlimpnfmpt  45941  climxlim2lem  45942  cncficcgt0  45985  cncfioobd  45994  fprodsubrecnncnvlem  46004  fprodaddrecnncnvlem  46006  dvmptmulf  46034  dvnmul  46040  dvmptfprodlem  46041  dvmptfprod  46042  dvnprodlem1  46043  dvnprodlem2  46044  iblsplitf  46067  itgperiod  46078  stoweidlem3  46100  stoweidlem26  46123  stoweidlem27  46124  stoweidlem29  46126  stoweidlem31  46128  stoweidlem34  46131  stoweidlem35  46132  stoweidlem36  46133  stoweidlem39  46136  stoweidlem42  46139  stoweidlem43  46140  stoweidlem44  46141  stoweidlem46  46143  stoweidlem48  46145  stoweidlem49  46146  stoweidlem51  46148  stoweidlem52  46149  stoweidlem53  46150  stoweidlem54  46151  stoweidlem55  46152  stoweidlem56  46153  stoweidlem57  46154  stoweidlem58  46155  stoweidlem59  46156  stoweidlem60  46157  stoweidlem61  46158  stoweidlem62  46159  stoweid  46160  wallispilem3  46164  stirlinglem13  46183  stirling  46186  fourierdlem16  46220  fourierdlem21  46225  fourierdlem22  46226  fourierdlem31  46235  fourierdlem39  46243  fourierdlem48  46251  fourierdlem51  46254  fourierdlem68  46271  fourierdlem71  46274  fourierdlem73  46276  fourierdlem80  46283  fourierdlem81  46284  fourierdlem86  46289  fourierdlem87  46290  fourierdlem93  46296  fourierdlem94  46297  fourierdlem103  46306  fourierdlem104  46307  fourierdlem112  46315  fourierdlem113  46316  elaa2  46331  etransclem32  46363  salexct  46431  sge0revalmpt  46475  sge0f1o  46479  sge0lefi  46495  sge0resplit  46503  sge0lempt  46507  sge0iunmptlemre  46512  sge0fodjrnlem  46513  sge0iunmpt  46515  sge0ltfirpmpt2  46523  sge0isum  46524  sge0xp  46526  sge0isummpt2  46529  sge0xadd  46532  sge0pnffsumgt  46539  sge0gtfsumgt  46540  sge0uzfsumgt  46541  sge0reuz  46544  sge0reuzb  46545  iundjiun  46557  meadjiun  46563  ismeannd  46564  voliunsge0lem  46569  meaiunincf  46580  meaiuninc3v  46581  meaiuninc3  46582  meaiininc  46584  caragenfiiuncl  46612  omeiunltfirp  46616  ovnsubaddlem2  46668  hoidmvval0  46684  hoidmvlelem1  46692  hoidmvlelem3  46694  hoidmvlelem5  46696  ovnlecvr2  46707  hspdifhsp  46713  hoiqssbllem2  46720  hoiqssbllem3  46721  hspmbllem2  46724  opnvonmbllem2  46730  hoimbl2  46762  vonhoire  46769  iinhoiicc  46771  iunhoiioolem  46772  iunhoiioo  46773  vonioo  46779  vonicc  46782  vonn0ioo2  46787  vonn0icc2  46789  salpreimagelt  46804  salpreimalegt  46806  pimincfltioc  46813  pimdecfgtioo  46814  pimincfltioo  46815  preimageiingt  46817  preimaleiinlt  46818  salpreimagtge  46822  salpreimaltle  46823  salpreimalelt  46826  salpreimagtlt  46827  incsmflem  46838  issmflelem  46841  issmfle  46842  smfconst  46846  issmfgtlem  46852  issmfgt  46853  smfaddlem2  46861  smfadd  46862  decsmflem  46863  decsmf  46864  issmfgelem  46866  issmfge  46867  smflimlem2  46869  smflim  46874  smfresal  46885  smfrec  46886  smfmullem4  46891  smfmul  46892  smfpimcc  46905  smflimmpt  46907  smfsuplem1  46908  smfsupmpt  46912  smfsupxr  46913  smfinflem  46914  smfinfmpt  46916  smflimsuplem5  46921  smflimsuplem7  46923  smflimsuplem8  46924  smflimsupmpt  46926  smfliminflem  46927  smfliminfmpt  46929  smfpimne2  46937  fsupdm  46939  smfsupdmmbllem  46941  finfdm  46943  smfinfdmmbllem  46945  or2expropbilem2  47132  or2expropbi  47133  cfsetsnfsetf  47157  2reu8i  47212  nfdfat  47226  iccelpart  47532  ichnfim  47563  ich2exprop  47570  ichreuopeq  47572  sprsymrelfo  47596  reupr  47621  reuopreuprim  47625  2zrngmmgm  48351  cbvmpox2  48435  ovmpordxf  48438  1arymaptfo  48743  2arymaptfo  48754  iinfssclem3  49156  iinfssc  49157  iinfsubc  49158  setrec1  49791  pgindnf  49816  aacllem  49901