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 849  df-tru 1543  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfnan  1900  nf3an  1901  hban  2300  nfeqf  2386  nfald2  2450  2ax6elem  2475  nfsb4t  2504  nfeu1ALT  2589  eupicka  2634  mopick2  2637  2mo  2648  nfabd2  2929  2ralbida  3283  r19.12  3314  r19.12OLD  3315  reean  3316  ralcom2  3377  cbvrmow  3409  nfrmow  3413  nfreuw  3414  cbvreuwOLD  3415  cbvreu  3428  cbvrabw  3473  cbvrabwOLD  3474  nfrabw  3475  cbvrab  3479  ceqsex2  3535  vtocl2gafOLD  3580  vtocl3gaf  3581  spc2ed  3601  rspce  3611  eqvincf  3650  elrabf  3688  elrab3t  3691  rexab2  3705  morex  3725  reu2  3731  rmo3f  3740  reu2eqd  3742  sbc2iegf  3865  reu8nf  3877  rmo2  3887  rmo3  3889  csbiebt  3928  csbie2t  3937  cbvrabcsfw  3940  cbvreucsf  3943  cbvrabcsf  3944  nfdif  4129  nfin  4224  reusngf  4674  rexreusng  4679  reuprg0  4702  rabsnifsb  4722  nfop  4889  nfopd  4890  eluniab  4921  iuneqconst  5003  cbvopab  5215  cbvopab1  5217  cbvopab1g  5218  cbvopab2  5219  cbvopab1s  5220  mpteq12f  5230  nfmpt  5249  cbvmptf  5251  cbvmptfg  5252  axrep3  5283  axrep4OLD  5286  axrep5  5287  reusv2lem3  5400  axprlem4OLD  5429  axprlem5OLD  5430  nfpo  5598  nfso  5599  nffr  5658  nfwe  5660  nfxp  5718  opeliunxp  5752  opeliun2xp  5753  nfco  5876  elrnmpt1  5971  nfimad  6087  reuop  6313  iota2  6550  nffun  6589  imadif  6650  nffn  6667  nff  6732  nff1  6802  nffo  6819  nff1o  6846  nffvd  6918  fv3  6924  funimassd  6975  fvmptdf  7022  fompt  7138  f1ossf1o  7148  fmptco  7149  fsnex  7303  nfiso  7342  nfriotadw  7396  cbvriotaw  7397  nfriotad  7399  cbvriota  7401  riota2df  7411  riota5f  7416  oprabv  7493  nfoprab  7497  mpoeq123  7505  nfmpo  7515  cbvoprab1  7520  cbvoprab2  7521  cbvoprab12  7522  cbvoprab3  7524  cbvmpox  7526  ovmpodxf  7583  elovmporab  7679  elovmporab1w  7680  elovmporab1  7681  onminex  7822  fiun  7967  f1iun  7968  opabex3d  7990  opabex3rd  7991  opabex3  7992  dfoprab4f  8081  fmpox  8092  opeliunxp2f  8235  nffrecs  8308  frrlem4  8314  nfwrecsOLD  8342  wfrlem4OLD  8352  tfr3  8439  tz7.49  8485  naddsuc2  8739  erovlem  8853  nfixpw  8956  nfixp  8957  nfixp1  8958  xpf1o  9179  nneneq  9246  nneneqOLD  9258  ac6sfi  9320  nfoi  9554  wdom2d  9620  infpssrlem4  10346  hsmexlem2  10467  hsmexlem4  10469  domtriomlem  10482  axdc3lem2  10491  axdc4lem  10495  zorn2lem4  10539  zorn2lem5  10540  konigthlem  10608  axextnd  10631  axrepndlem2  10633  axrepnd  10634  axunnd  10636  axpowndlem2  10638  axpowndlem4  10640  axpownd  10641  axregndlem2  10643  axregnd  10644  axinfndlem1  10645  axinfnd  10646  zfcndrep  10654  zfcndinf  10658  dedekind  11424  dedekindle  11425  fsuppmapnn0fiublem  14031  fsuppmapnn0fiub  14032  fsuppmapnn0fiubex  14033  reuccatpfxs1  14785  nfsum1  15726  nfsum  15727  fsumclf  15774  fsumsplitf  15778  fsumsplit1  15781  fsum2dlem  15806  fsum00  15834  nfcprod1  15944  nfcprod  15945  fprod2dlem  16016  fprodsplitf  16024  fprodsplit1f  16026  fprodle  16032  lcmfunsnlem1  16674  lcmfunsnlem2lem1  16675  lcmfunsnlem2  16677  mreexexd  17691  acsmapd  18599  gsum2d2lem  19991  dprd2d2  20064  gsummoncoe1  22312  gsummatr01lem4  22664  cpmatmcllem  22724  cayleyhamilton1  22898  neiptopnei  23140  neiptopreu  23141  neitr  23188  iunconnlem  23435  iunconn  23436  ptcnplem  23629  ptcnp  23630  xkocnv  23822  isfildlem  23865  utopsnneiplem  24256  isucn2  24288  cfilucfil  24572  restmetu  24583  ovolfiniun  25536  ovoliunlem3  25539  ovoliunnul  25542  volfiniun  25582  itg2splitlem  25783  itg2split  25784  isibl2  25801  nfitg  25810  cbvitg  25811  limciun  25929  2sqmo  27481  2sqreulem4  27498  istrkg2ld  28468  chirred  32414  sbc2iedf  32484  rspc2daf  32485  opreu2reuALT  32496  mo5f  32508  foresf1o  32523  iinabrex  32582  cbvdisjf  32584  disjabrex  32595  disjabrexf  32596  funimass4f  32647  2ndresdju  32659  fmptcof2  32667  fcomptf  32668  acunirnmpt2  32670  acunirnmpt2f  32671  aciunf1lem  32672  funcnv4mpt  32679  fnpreimac  32681  f1od2  32732  fpwrelmap  32744  xrofsup  32771  nn0min  32822  fprodex01  32827  fsumiunle  32831  prodindf  32848  elrgspnsubrunlem2  33252  isarchiofld  33347  nsgqusf1olem1  33441  nsgqusf1olem3  33443  elrspunidl  33456  fedgmullem2  33681  irngnzply1  33741  reff  33838  locfinreflem  33839  cmpcref  33849  zarclsiin  33870  zarcmplem  33880  ordtconnlem1  33923  esumcl  34031  gsumesum  34060  esumlub  34061  esumcst  34064  esumrnmpt2  34069  esumfzf  34070  esumfsup  34071  hasheuni  34086  esumcvg  34087  esumgect  34091  esumcvgre  34092  esum2dlem  34093  esum2d  34094  esumiun  34095  ldsysgenld  34161  sigapildsyslem  34162  sigapildsys  34163  ldgenpisyslem1  34164  measvunilem  34213  measvunilem0  34214  measvuni  34215  measinblem  34221  voliune  34230  volfiniune  34231  volmeas  34232  oms0  34299  omssubadd  34302  eulerpartlemgvv  34378  dstrvprob  34474  breprexplema  34645  bnj919  34781  bnj1146  34805  bnj1379  34844  bnj849  34939  bnj916  34947  bnj964  34957  bnj1014  34975  bnj1123  35000  bnj1228  35025  bnj1307  35037  bnj1321  35041  bnj1398  35048  bnj1408  35050  bnj1444  35057  bnj1445  35058  bnj1446  35059  bnj1449  35062  bnj1467  35068  bnj1463  35069  bnj1489  35070  bnj1491  35071  bnj1312  35072  bnj1525  35083  dvelimalcased  35089  dvelimexcased  35091  fineqvrep  35109  cvmcov  35268  iota5f  35724  axextdist  35800  axextbdist  35801  nfwlim  35823  finminlem  36319  bj-dvelimdv  36852  bj-opabco  37189  isbasisrelowllem1  37356  isbasisrelowllem2  37357  fvineqsneu  37412  fvineqsneq  37413  wl-cbvalnaed  37533  wl-2sb6d  37559  wl-sbalnae  37563  wl-mo2tf  37572  wl-eutf  37574  wl-ax11-lem3  37588  phpreu  37611  poimirlem26  37653  poimirlem27  37654  heicant  37662  mbfposadd  37674  ftc1anclem5  37704  indexdom  37741  filbcmb  37747  sdclem2  37749  sdclem1  37750  fdc1  37753  riotasv2d  38958  riotasv2s  38959  nfded2  38969  glbconxN  39380  pmapglb2xN  39774  cdlemefs32sn1aw  40416  mzpsubmpt  42754  mzpexpmpt  42756  eq0rabdioph  42787  eqrabdioph  42788  setindtr  43036  unielss  43230  nadd1suc  43405  ss2iundf  43672  scottabf  44259  mnuprdlem4  44294  ismnushort  44320  binomcxplemnotnn0  44375  iunconnlem2  44955  nfrelp  44970  modelaxreplem3  44997  modelaxrep  44998  elunif  45021  rspcegf  45028  fnchoice  45034  refsumcn  45035  rfcnnnub  45041  uzwo4  45058  fiiuncl  45070  cbvmpo2  45102  cbvmpo1  45103  iinssiin  45134  disjf1  45188  disjrnmpt2  45193  disjf1o  45196  disjinfi  45197  choicefi  45205  axccdom  45227  dmrelrnrel  45231  axccd  45234  rnmptbddlem  45251  rnmptbd2lem  45255  infnsuprnmpt  45257  rnmptbdlem  45262  rnmptssbi  45267  upbdrech  45317  ssfiunibd  45321  supxrgere  45344  supxrgelem  45348  supxrge  45349  xralrple2  45365  infxr  45378  infxrunb2  45379  xrralrecnnle  45394  xrralrecnnge  45401  supxrunb3  45410  supxrleubrnmpt  45417  infleinf2  45425  unb2ltle  45426  rexabslelem  45429  suprleubrnmpt  45433  uzub  45442  supminfrnmpt  45456  supxrleubrnmptf  45462  infxrgelbrnmpt  45465  infrpgernmpt  45476  monoordxr  45493  monoord2xr  45495  caucvgbf  45500  cvgcaule  45502  iccshift  45531  iooshift  45535  iooiinicc  45555  iooiinioc  45569  fsummulc1f  45586  fsumf1of  45589  fsumreclf  45591  fsumlessf  45592  fmul01  45595  fmuldfeqlem1  45597  fmuldfeq  45598  fmul01lt1lem1  45599  fmul01lt1lem2  45600  fprodexp  45609  mccl  45613  fprodcnlem  45614  fprodcn  45615  climmulf  45619  climexp  45620  climsuse  45623  climrecf  45624  climinff  45626  climaddf  45630  mullimc  45631  islptre  45634  climf  45637  mullimcf  45638  rexlim2d  45640  idlimc  45641  limcperiod  45643  limcrecl  45644  islpcn  45654  limsupre  45656  limcleqr  45659  addlimc  45663  limclner  45666  climsubmpt  45675  climreclf  45679  climf2  45681  climeldmeqmpt  45683  clim2f2  45685  climfveqmpt  45686  fnlimfvre  45689  allbutfifvre  45690  climleltrp  45691  fnlimf  45693  fnlimabslt  45694  climfveqf  45695  climfveqmpt3  45697  climeldmeqf  45698  climeqf  45703  climeldmeqmpt3  45704  limsuppnfd  45717  limsupub  45719  climinf2lem  45721  climinf2  45722  limsuppnf  45726  limsupubuz  45728  climinf2mpt  45729  climinfmpt  45730  climinf3  45731  limsupmnflem  45735  limsupequz  45738  limsupre2  45740  limsupmnfuzlem  45741  limsupequzmptf  45746  limsupre3  45748  limsupre3uzlem  45750  limsupreuzmpt  45754  climisp  45761  lmbr3  45762  climrescn  45763  climxrrelem  45764  climxrre  45765  limsupub2  45827  liminflbuz2  45830  xlimmnfvlem2  45848  xlimmnfv  45849  xlimpnfvlem2  45852  xlimpnfv  45853  xlimmnfmpt  45858  xlimpnfmpt  45859  climxlim2lem  45860  cncficcgt0  45903  cncfioobd  45912  fprodsubrecnncnvlem  45922  fprodaddrecnncnvlem  45924  dvmptmulf  45952  dvnmul  45958  dvmptfprodlem  45959  dvmptfprod  45960  dvnprodlem1  45961  dvnprodlem2  45962  iblsplitf  45985  itgperiod  45996  stoweidlem3  46018  stoweidlem26  46041  stoweidlem27  46042  stoweidlem29  46044  stoweidlem31  46046  stoweidlem34  46049  stoweidlem35  46050  stoweidlem36  46051  stoweidlem39  46054  stoweidlem42  46057  stoweidlem43  46058  stoweidlem44  46059  stoweidlem46  46061  stoweidlem48  46063  stoweidlem49  46064  stoweidlem51  46066  stoweidlem52  46067  stoweidlem53  46068  stoweidlem54  46069  stoweidlem55  46070  stoweidlem56  46071  stoweidlem57  46072  stoweidlem58  46073  stoweidlem59  46074  stoweidlem60  46075  stoweidlem61  46076  stoweidlem62  46077  stoweid  46078  wallispilem3  46082  stirlinglem13  46101  stirling  46104  fourierdlem16  46138  fourierdlem21  46143  fourierdlem22  46144  fourierdlem31  46153  fourierdlem39  46161  fourierdlem48  46169  fourierdlem51  46172  fourierdlem68  46189  fourierdlem71  46192  fourierdlem73  46194  fourierdlem80  46201  fourierdlem81  46202  fourierdlem86  46207  fourierdlem87  46208  fourierdlem93  46214  fourierdlem94  46215  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  fourierdlem113  46234  elaa2  46249  etransclem32  46281  salexct  46349  sge0revalmpt  46393  sge0f1o  46397  sge0lefi  46413  sge0resplit  46421  sge0lempt  46425  sge0iunmptlemre  46430  sge0fodjrnlem  46431  sge0iunmpt  46433  sge0ltfirpmpt2  46441  sge0isum  46442  sge0xp  46444  sge0isummpt2  46447  sge0xadd  46450  sge0pnffsumgt  46457  sge0gtfsumgt  46458  sge0uzfsumgt  46459  sge0reuz  46462  sge0reuzb  46463  iundjiun  46475  meadjiun  46481  ismeannd  46482  voliunsge0lem  46487  meaiunincf  46498  meaiuninc3v  46499  meaiuninc3  46500  meaiininc  46502  caragenfiiuncl  46530  omeiunltfirp  46534  ovnsubaddlem2  46586  hoidmvval0  46602  hoidmvlelem1  46610  hoidmvlelem3  46612  hoidmvlelem5  46614  ovnlecvr2  46625  hspdifhsp  46631  hoiqssbllem2  46638  hoiqssbllem3  46639  hspmbllem2  46642  opnvonmbllem2  46648  hoimbl2  46680  vonhoire  46687  iinhoiicc  46689  iunhoiioolem  46690  iunhoiioo  46691  vonioo  46697  vonicc  46700  vonn0ioo2  46705  vonn0icc2  46707  salpreimagelt  46722  salpreimalegt  46724  pimincfltioc  46731  pimdecfgtioo  46732  pimincfltioo  46733  preimageiingt  46735  preimaleiinlt  46736  salpreimagtge  46740  salpreimaltle  46741  salpreimalelt  46744  salpreimagtlt  46745  incsmflem  46756  issmflelem  46759  issmfle  46760  smfconst  46764  issmfgtlem  46770  issmfgt  46771  smfaddlem2  46779  smfadd  46780  decsmflem  46781  decsmf  46782  issmfgelem  46784  issmfge  46785  smflimlem2  46787  smflim  46792  smfresal  46803  smfrec  46804  smfmullem4  46809  smfmul  46810  smfpimcc  46823  smflimmpt  46825  smfsuplem1  46826  smfsupmpt  46830  smfsupxr  46831  smfinflem  46832  smfinfmpt  46834  smflimsuplem5  46839  smflimsuplem7  46841  smflimsuplem8  46842  smflimsupmpt  46844  smfliminflem  46845  smfliminfmpt  46847  smfpimne2  46855  fsupdm  46857  smfsupdmmbllem  46859  finfdm  46861  smfinfdmmbllem  46863  or2expropbilem2  47045  or2expropbi  47046  cfsetsnfsetf  47070  2reu8i  47125  nfdfat  47139  iccelpart  47420  ichnfim  47451  ich2exprop  47458  ichreuopeq  47460  sprsymrelfo  47484  reupr  47509  reuopreuprim  47513  2zrngmmgm  48168  cbvmpox2  48252  ovmpordxf  48255  1arymaptfo  48564  2arymaptfo  48575  setrec1  49210  pgindnf  49235  aacllem  49320