Theorem nfan 1932

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

This proof depends on syntax axioms:   ∧ wa 401  ⊤wtru 1571  Ⅎwnf 1816

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

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817

This theorem is used by:  nfnan  1933  nf3an  1934  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  4076  nfin  4169  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  5561  nfso  5562  nffr  5620  nfwe  5622  nfxp  5680  opeliunxp  5714  opeliun2xp  5715  nfco  5839  elrnmpt1  5938  nfimad  6059  reuop  6285  iota2  6516  nffun  6550  imadif  6612  nffn  6626  nff  6693  nff1  6764  nffo  6783  nff1o  6810  nffvd  6885  fv3  6891  funimassd  6939  fvmptdf  6988  fompt  7106  f1ossf1o  7117  fmptco  7118  fsnex  7279  nfiso  7318  nfriotadw  7373  cbvriotaw  7374  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  7558  elovmporab  7655  elovmporab1w  7656  elovmporab1  7657  onminex  7799  fiun  7938  f1iun  7939  opabex3d  7960  opabex3rd  7961  opabex3  7962  dfoprab4f  8050  fmpox  8061  opeliunxp2f  8205  nffrecs  8279  frrlem4  8285  tfr3  8385  tz7.49  8433  naddsuc2  8689  erovlem  8812  nfixpw  8922  nfixp  8923  nfixp1  8924  xpf1o  9136  nneneq  9199  ac6sfi  9253  nfoi  9486  wdom2d  9552  scottabf  9911  setrec1  9944  infpssrlem4  10356  hsmexlem2  10477  hsmexlem4  10479  domtriomlem  10492  axdc3lem2  10501  axdc4lem  10505  zorn2lem4  10549  zorn2lem5  10550  konigthlem  10625  axextnd  10648  axrepndlem2  10650  axrepnd  10651  axunnd  10653  axpowndlem2  10655  axpowndlem4  10657  axpownd  10658  axregndlem2  10660  axregnd  10661  axinfndlem1  10662  axinfnd  10663  zfcndrep  10671  zfcndinf  10675  dedekind  11445  dedekindle  11446  fsuppmapnn0fiublem  14102  fsuppmapnn0fiub  14103  fsuppmapnn0fiubex  14104  reuccatpfxs1  14864  nfsum1  15825  nfsum  15826  fsumclf  15872  fsumsplitf  15876  fsumsplit1  15879  fsum2dlem  15904  fsum00  15933  nfcprod1  16045  nfcprod  16046  fprod2dlem  16115  fprodsplitf  16123  fprodsplit1f  16125  fprodle  16131  lcmfunsnlem1  16775  lcmfunsnlem2lem1  16776  lcmfunsnlem2  16778  mreexexd  17784  acsmapd  18690  gsum2d2lem  20149  dprd2d2  20222  gsummoncoe1  22588  gsummatr01lem4  22935  cpmatmcllem  22998  cayleyhamilton1  23172  neiptopnei  23412  neiptopreu  23413  neitr  23460  iunconnlem  23707  iunconn  23708  ptcnplem  23902  ptcnp  23903  xkocnv  24095  isfildlem  24138  utopsnneiplem  24528  isucn2  24559  cfilucfil  24840  restmetu  24851  ovolfiniun  25784  ovoliunlem3  25787  ovoliunnul  25790  volfiniun  25830  itg2splitlem  26031  itg2split  26032  isibl2  26049  nfitg  26057  cbvitg  26058  limciun  26176  2sqmo  27728  2sqreulem4  27745  bdaypw2n0bndlem  28783  istrkg2ld  28856  chirred  32931  sbc2iedf  32996  rspc2daf  32997  opreu2reuALT  33007  mo5f  33019  foresf1o  33034  iinabrex  33097  cbvdisjf  33099  disjabrex  33110  disjabrexf  33111  funimass4f  33165  2ndresdju  33177  fmptcof2  33185  fcomptf  33186  acunirnmpt2  33188  acunirnmpt2f  33189  aciunf1lem  33190  funcnv4mpt  33196  fnpreimac  33198  f1od2  33245  fpwrelmap  33259  xrofsup  33293  nn0min  33346  fprodex01  33350  fsumiunle  33354  prodindf  33363  suppgsumssiun  33567  isarchiofld  33694  elrgspnsubrunlem2  33743  nsgqusf1olem1  33898  nsgqusf1olem3  33900  elrspunidl  33912  deg1prod  34049  mplvrpmga  34111  esplyfval1  34139  vieta  34146  fedgmullem2  34196  irngnzply1  34257  reff  34405  locfinreflem  34406  cmpcref  34416  zarclsiin  34437  zarcmplem  34447  ordtconnlem1  34490  esumcl  34596  gsumesum  34625  esumlub  34626  esumcst  34629  esumrnmpt2  34634  esumfzf  34635  esumfsup  34636  hasheuni  34651  esumcvg  34652  esumgect  34656  esumcvgre  34657  esum2dlem  34658  esum2d  34659  esumiun  34660  ldsysgenld  34727  sigapildsyslem  34728  sigapildsys  34729  ldgenpisyslem1  34730  measvunilem  34779  measvunilem0  34780  measvuni  34781  measinblem  34787  voliune  34796  volfiniune  34797  volmeas  34798  oms0  34864  omssubadd  34867  eulerpartlemgvv  34943  dstrvprob  35039  breprexplema  35194  bnj919  35333  bnj1146  35356  bnj1379  35395  bnj849  35490  bnj916  35498  bnj964  35508  bnj1014  35526  bnj1123  35551  bnj1228  35576  bnj1307  35588  bnj1321  35592  bnj1398  35599  bnj1408  35601  bnj1444  35608  bnj1445  35609  bnj1446  35610  bnj1449  35613  bnj1467  35619  bnj1463  35620  bnj1489  35621  bnj1491  35622  bnj1312  35623  bnj1525  35634  dvelimalcased  35640  dvelimexcased  35642  fineqvrep  35707  cvmcov  35949  iota5f  36410  axextdist  36483  axextbdist  36484  nfwlim  36506  finminlem  37028  axtcond  37188  mh-inf3f1  37251  bj-dvelimdv  37685  bj-axreprepsep  37911  bj-opabco  38029  isbasisrelowllem1  38198  isbasisrelowllem2  38199  fvineqsneu  38254  fvineqsneq  38255  wl-cbvalnaed  38384  wl-2sb6d  38410  wl-sbalnae  38414  wl-mo2tf  38423  wl-eutf  38425  phpreu  38447  poimirlem26  38484  poimirlem27  38485  heicant  38493  mbfposadd  38505  ftc1anclem5  38535  indexdom  38588  filbcmb  38594  sdclem2  38596  sdclem1  38597  fdc1  38600  riotasv2d  39934  riotasv2s  39935  nfded2  39945  glbconxN  40355  pmapglb2xN  40749  cdlemefs32sn1aw  41391  mzpsubmpt  43692  mzpexpmpt  43694  eq0rabdioph  43725  eqrabdioph  43726  setindtr  43969  unielss  44163  nadd1suc  44337  ss2iundf  44603  mnuprdlem4  45203  ismnushort  45229  binomcxplemnotnn0  45284  iunconnlem2  45861  nfrelp  45876  modelaxreplem3  45907  modelaxrep  45908  permaxrep  45933  elunif  45954  rspcegf  45961  fnchoice  45967  refsumcn  45968  rfcnnnub  45974  uzwo4  45991  fiiuncl  46003  cbvmpo2  46033  cbvmpo1  46034  iinssiin  46065  disjf1  46119  disjrnmpt2  46124  disjf1o  46127  disjinfi  46128  choicefi  46135  axccdom  46156  dmrelrnrel  46160  axccd  46162  rnmptbddlem  46177  rnmptbd2lem  46181  infnsuprnmpt  46183  rnmptbdlem  46188  rnmptssbi  46193  upbdrech  46242  ssfiunibd  46246  supxrgere  46267  supxrgelem  46271  supxrge  46272  xralrple2  46288  infxr  46300  infxrunb2  46301  xrralrecnnle  46316  xrralrecnnge  46323  supxrunb3  46332  supxrleubrnmpt  46338  infleinf2  46346  unb2ltle  46347  rexabslelem  46350  suprleubrnmpt  46354  uzub  46363  supminfrnmpt  46377  supxrleubrnmptf  46383  infxrgelbrnmpt  46386  infrpgernmpt  46397  monoordxr  46414  monoord2xr  46416  caucvgbf  46421  cvgcaule  46423  iccshift  46452  iooshift  46456  iooiinicc  46476  iooiinioc  46490  fsummulc1f  46505  fsumf1of  46508  fsumreclf  46510  fsumlessf  46511  fmul01  46514  fmuldfeqlem1  46516  fmuldfeq  46517  fmul01lt1lem1  46518  fmul01lt1lem2  46519  fprodexp  46528  mccl  46532  fprodcnlem  46533  fprodcn  46534  climmulf  46538  climexp  46539  climsuse  46542  climrecf  46543  climinff  46545  climaddf  46549  mullimc  46550  islptre  46553  climf  46556  mullimcf  46557  rexlim2d  46559  idlimc  46560  limcperiod  46562  limcrecl  46563  islpcn  46571  limsupre  46573  limcleqr  46576  addlimc  46580  limclner  46583  climsubmpt  46592  climreclf  46596  climf2  46598  climeldmeqmpt  46600  clim2f2  46602  climfveqmpt  46603  fnlimfvre  46606  allbutfifvre  46607  climleltrp  46608  fnlimf  46610  fnlimabslt  46611  climfveqf  46612  climfveqmpt3  46614  climeldmeqf  46615  climeqf  46620  climeldmeqmpt3  46621  limsuppnfd  46634  limsupub  46636  climinf2lem  46638  climinf2  46639  limsuppnf  46643  limsupubuz  46645  climinf2mpt  46646  climinfmpt  46647  climinf3  46648  limsupmnflem  46652  limsupequz  46655  limsupre2  46657  limsupmnfuzlem  46658  limsupequzmptf  46663  limsupre3  46665  limsupre3uzlem  46667  limsupreuzmpt  46671  climisp  46678  lmbr3  46679  climrescn  46680  climxrrelem  46681  climxrre  46682  limsupub2  46744  liminflbuz2  46747  xlimmnfvlem2  46765  xlimmnfv  46766  xlimpnfvlem2  46769  xlimpnfv  46770  xlimmnfmpt  46775  xlimpnfmpt  46776  climxlim2lem  46777  cncficcgt0  46820  cncfioobd  46829  fprodsubrecnncnvlem  46839  fprodaddrecnncnvlem  46841  dvmptmulf  46869  dvnmul  46875  dvmptfprodlem  46876  dvmptfprod  46877  dvnprodlem1  46878  dvnprodlem2  46879  iblsplitf  46902  itgperiod  46913  stoweidlem3  46935  stoweidlem26  46958  stoweidlem27  46959  stoweidlem29  46961  stoweidlem31  46963  stoweidlem34  46966  stoweidlem35  46967  stoweidlem36  46968  stoweidlem39  46971  stoweidlem42  46974  stoweidlem43  46975  stoweidlem44  46976  stoweidlem46  46978  stoweidlem48  46980  stoweidlem49  46981  stoweidlem51  46983  stoweidlem52  46984  stoweidlem53  46985  stoweidlem54  46986  stoweidlem55  46987  stoweidlem56  46988  stoweidlem57  46989  stoweidlem58  46990  stoweidlem59  46991  stoweidlem60  46992  stoweidlem61  46993  stoweidlem62  46994  stoweid  46995  wallispilem3  46999  stirlinglem13  47018  stirling  47021  fourierdlem16  47055  fourierdlem21  47060  fourierdlem22  47061  fourierdlem31  47070  fourierdlem39  47078  fourierdlem48  47086  fourierdlem51  47089  fourierdlem68  47106  fourierdlem71  47109  fourierdlem73  47111  fourierdlem80  47118  fourierdlem81  47119  fourierdlem86  47124  fourierdlem87  47125  fourierdlem93  47131  fourierdlem94  47132  fourierdlem103  47141  fourierdlem104  47142  fourierdlem112  47150  fourierdlem113  47151  elaa2  47166  etransclem32  47198  salexct  47266  sge0revalmpt  47310  sge0f1o  47314  sge0lefi  47330  sge0resplit  47338  sge0lempt  47342  sge0iunmptlemre  47347  sge0fodjrnlem  47348  sge0iunmpt  47350  sge0ltfirpmpt2  47358  sge0isum  47359  sge0xp  47361  sge0isummpt2  47364  sge0xadd  47367  sge0pnffsumgt  47374  sge0gtfsumgt  47375  sge0uzfsumgt  47376  sge0reuz  47379  sge0reuzb  47380  iundjiun  47392  meadjiun  47398  ismeannd  47399  voliunsge0lem  47404  meaiunincf  47415  meaiuninc3v  47416  meaiuninc3  47417  meaiininc  47419  caragenfiiuncl  47447  omeiunltfirp  47451  ovnsubaddlem2  47503  hoidmvval0  47519  hoidmvlelem1  47527  hoidmvlelem3  47529  hoidmvlelem5  47531  ovnlecvr2  47542  hspdifhsp  47548  hoiqssbllem2  47555  hoiqssbllem3  47556  hspmbllem2  47559  opnvonmbllem2  47565  hoimbl2  47597  vonhoire  47604  iinhoiicc  47606  iunhoiioolem  47607  iunhoiioo  47608  vonioo  47614  vonicc  47617  vonn0ioo2  47622  vonn0icc2  47624  salpreimagelt  47639  salpreimalegt  47641  pimincfltioc  47648  pimdecfgtioo  47649  pimincfltioo  47650  preimageiingt  47652  preimaleiinlt  47653  salpreimagtge  47657  salpreimaltle  47658  salpreimalelt  47661  salpreimagtlt  47662  incsmflem  47673  issmflelem  47676  issmfle  47677  smfconst  47681  issmfgtlem  47687  issmfgt  47688  smfaddlem2  47696  smfadd  47697  decsmflem  47698  decsmf  47699  issmfgelem  47701  issmfge  47702  smflimlem2  47704  smflim  47709  smfresal  47720  smfrec  47721  smfmullem4  47726  smfmul  47727  smfpimcc  47740  smflimmpt  47742  smfsuplem1  47743  smfsupmpt  47747  smfsupxr  47748  smfinflem  47749  smfinfmpt  47751  smflimsuplem5  47756  smflimsuplem7  47758  smflimsuplem8  47759  smflimsupmpt  47761  smfliminflem  47762  smfliminfmpt  47764  smfpimne2  47772  fsupdm  47774  smfsupdmmbllem  47776  finfdm  47778  smfinfdmmbllem  47780  or2expropbilem2  48025  or2expropbi  48026  cfsetsnfsetf  48050  2reu8i  48105  nfdfat  48119  iccelpart  48437  ichnfim  48468  ich2exprop  48475  ichreuopeq  48477  sprsymrelfo  48501  reupr  48526  reuopreuprim  48530  2zrngmmgm  49271  cbvmpox2  49370  ovmpordxf  49373  1arymaptfo  49677  2arymaptfo  49688  iinfssclem3  50086  iinfssc  50087  iinfsubc  50088  pgindnf  50731  nfals  50821  nfrals  50822  nfalseu  50852  nfralseu  50853  aacllem  50861