Theorem nfan 1922

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

Syntax hints:   ∧ wa 400  ⊤wtru 1564  Ⅎwnf 1806

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-nf 1807

This theorem is referenced by:  nfnan  1923  nf3an  1924  hban  2337  nfeqf  2415  nfald2  2479  2ax6elem  2504  nfsb4t  2533  nfeu1  2619  eupicka  2664  mopick2  2667  2mo  2678  nfabd2  2950  2ralbida  3288  r19.12  3314  reean  3315  ralcom2  3367  cbvrmow  3395  nfrmow  3399  nfreuw  3400  cbvreu  3409  cbvrabw  3452  cbvrabwOLD  3453  nfrabw  3454  cbvrab  3456  ceqsex2  3507  vtocl3gaf  3547  spc2ed  3563  rspce  3573  eqvincf  3612  elrabf  3650  elrab3t  3652  rexab2  3665  morex  3685  reu2  3691  rmo3f  3700  reu2eqd  3702  sbc2iegf  3821  reu8nf  3833  rmo2  3843  rmo3  3845  csbiebt  3884  csbie2t  3893  cbvrabcsfw  3896  cbvreucsf  3899  cbvrabcsf  3900  nfdif  4086  nfin  4179  reusngf  4636  rexreusng  4641  reuprg0  4664  rabsnifsb  4684  nfop  4850  nfopd  4851  eluniab  4882  iuneqconst  4964  cbvopab  5177  cbvopab1  5179  cbvopab1g  5180  cbvopab2  5181  cbvopab1s  5182  mpteq12f  5190  nfmpt  5203  cbvmptf  5205  cbvmptfg  5206  axrep3  5236  axrep4OLD  5239  axrep5  5240  reusv2lem3  5362  axprlem4OLD  5392  axprlem5OLD  5393  nfpo  5566  nfso  5567  nffr  5625  nfwe  5627  nfxp  5685  opeliunxp  5719  opeliun2xp  5720  nfco  5842  elrnmpt1  5941  nfimad  6062  reuop  6284  iota2  6514  nffun  6548  imadif  6609  nffn  6624  nff  6691  nff1  6762  nffo  6781  nff1o  6808  nffvd  6883  fv3  6889  funimassd  6937  fvmptdf  6986  fompt  7103  f1ossf1o  7114  fmptco  7115  fsnex  7271  nfiso  7310  nfriotadw  7365  cbvriotaw  7366  nfriotad  7368  cbvriota  7370  riota2df  7380  riota5f  7385  oprabv  7460  nfoprab  7464  mpoeq123  7472  nfmpo  7482  cbvoprab1  7487  cbvoprab2  7488  cbvoprab12  7489  cbvoprab3  7491  cbvmpox  7493  ovmpodxf  7550  elovmporab  7646  elovmporab1w  7647  elovmporab1  7648  onminex  7789  fiun  7928  f1iun  7929  opabex3d  7950  opabex3rd  7951  opabex3  7952  dfoprab4f  8041  fmpox  8052  opeliunxp2f  8194  nffrecs  8268  frrlem4  8274  tfr3  8374  tz7.49  8420  naddsuc2  8676  erovlem  8799  nfixpw  8902  nfixp  8903  nfixp1  8904  xpf1o  9115  nneneq  9178  ac6sfi  9232  nfoi  9464  wdom2d  9530  scottabf  9854  infpssrlem4  10278  hsmexlem2  10399  hsmexlem4  10401  domtriomlem  10414  axdc3lem2  10423  axdc4lem  10427  zorn2lem4  10471  zorn2lem5  10472  konigthlem  10541  axextnd  10564  axrepndlem2  10566  axrepnd  10567  axunnd  10569  axpowndlem2  10571  axpowndlem4  10573  axpownd  10574  axregndlem2  10576  axregnd  10577  axinfndlem1  10578  axinfnd  10579  zfcndrep  10587  zfcndinf  10591  dedekind  11361  dedekindle  11362  fsuppmapnn0fiublem  14017  fsuppmapnn0fiub  14018  fsuppmapnn0fiubex  14019  reuccatpfxs1  14774  nfsum1  15731  nfsum  15732  fsumclf  15779  fsumsplitf  15783  fsumsplit1  15786  fsum2dlem  15811  fsum00  15840  nfcprod1  15952  nfcprod  15953  fprod2dlem  16024  fprodsplitf  16032  fprodsplit1f  16034  fprodle  16040  lcmfunsnlem1  16685  lcmfunsnlem2lem1  16686  lcmfunsnlem2  16688  mreexexd  17694  acsmapd  18600  gsum2d2lem  20034  dprd2d2  20107  gsummoncoe1  22429  gsummatr01lem4  22776  cpmatmcllem  22836  cayleyhamilton1  23010  neiptopnei  23250  neiptopreu  23251  neitr  23298  iunconnlem  23545  iunconn  23546  ptcnplem  23739  ptcnp  23740  xkocnv  23932  isfildlem  23975  utopsnneiplem  24365  isucn2  24396  cfilucfil  24677  restmetu  24688  ovolfiniun  25621  ovoliunlem3  25624  ovoliunnul  25627  volfiniun  25667  itg2splitlem  25868  itg2split  25869  isibl2  25886  nfitg  25895  cbvitg  25896  limciun  26014  2sqmo  27559  2sqreulem4  27576  bdaypw2n0bndlem  28614  istrkg2ld  28687  chirred  32656  sbc2iedf  32722  rspc2daf  32723  opreu2reuALT  32733  mo5f  32745  foresf1o  32760  iinabrex  32824  cbvdisjf  32826  disjabrex  32837  disjabrexf  32838  funimass4f  32894  2ndresdju  32906  fmptcof2  32914  fcomptf  32915  acunirnmpt2  32917  acunirnmpt2f  32918  aciunf1lem  32919  funcnv4mpt  32925  fnpreimac  32927  f1od2  32976  fpwrelmap  32990  xrofsup  33024  nn0min  33078  fprodex01  33082  fsumiunle  33086  prodindf  33095  suppgsumssiun  33305  isarchiofld  33432  elrgspnsubrunlem2  33481  nsgqusf1olem1  33638  nsgqusf1olem3  33640  elrspunidl  33652  deg1prod  33790  mplvrpmga  33852  esplyfval1  33880  vieta  33887  fedgmullem2  33937  irngnzply1  33998  reff  34146  locfinreflem  34147  cmpcref  34157  zarclsiin  34178  zarcmplem  34188  ordtconnlem1  34231  esumcl  34337  gsumesum  34366  esumlub  34367  esumcst  34370  esumrnmpt2  34375  esumfzf  34376  esumfsup  34377  hasheuni  34392  esumcvg  34393  esumgect  34397  esumcvgre  34398  esum2dlem  34399  esum2d  34400  esumiun  34401  ldsysgenld  34467  sigapildsyslem  34468  sigapildsys  34469  ldgenpisyslem1  34470  measvunilem  34519  measvunilem0  34520  measvuni  34521  measinblem  34527  voliune  34536  volfiniune  34537  volmeas  34538  oms0  34604  omssubadd  34607  eulerpartlemgvv  34683  dstrvprob  34779  breprexplema  34934  bnj919  35073  bnj1146  35096  bnj1379  35135  bnj849  35230  bnj916  35238  bnj964  35248  bnj1014  35266  bnj1123  35291  bnj1228  35316  bnj1307  35328  bnj1321  35332  bnj1398  35339  bnj1408  35341  bnj1444  35348  bnj1445  35349  bnj1446  35350  bnj1449  35353  bnj1467  35359  bnj1463  35360  bnj1489  35361  bnj1491  35362  bnj1312  35363  bnj1525  35374  dvelimalcased  35380  dvelimexcased  35382  fineqvrep  35422  cvmcov  35626  iota5f  36087  axextdist  36160  axextbdist  36161  nfwlim  36183  finminlem  36691  axtcond  36851  bj-dvelimdv  37348  bj-axreprepsep  37572  bj-opabco  37692  isbasisrelowllem1  37861  isbasisrelowllem2  37862  fvineqsneu  37917  fvineqsneq  37918  wl-cbvalnaed  38047  wl-2sb6d  38073  wl-sbalnae  38077  wl-mo2tf  38086  wl-eutf  38088  phpreu  38115  poimirlem26  38157  poimirlem27  38158  heicant  38166  mbfposadd  38178  ftc1anclem5  38208  indexdom  38245  filbcmb  38251  sdclem2  38253  sdclem1  38254  fdc1  38257  riotasv2d  39593  riotasv2s  39594  nfded2  39604  glbconxN  40014  pmapglb2xN  40408  cdlemefs32sn1aw  41050  mzpsubmpt  43336  mzpexpmpt  43338  eq0rabdioph  43369  eqrabdioph  43370  setindtr  43613  unielss  43807  nadd1suc  43981  ss2iundf  44247  mnuprdlem4  44849  ismnushort  44875  binomcxplemnotnn0  44930  iunconnlem2  45508  nfrelp  45523  modelaxreplem3  45554  modelaxrep  45555  permaxrep  45580  elunif  45594  rspcegf  45601  fnchoice  45607  refsumcn  45608  rfcnnnub  45614  uzwo4  45631  fiiuncl  45643  cbvmpo2  45673  cbvmpo1  45674  iinssiin  45705  disjf1  45759  disjrnmpt2  45764  disjf1o  45767  disjinfi  45768  choicefi  45775  axccdom  45796  dmrelrnrel  45800  axccd  45802  rnmptbddlem  45817  rnmptbd2lem  45821  infnsuprnmpt  45823  rnmptbdlem  45828  rnmptssbi  45833  upbdrech  45882  ssfiunibd  45886  supxrgere  45907  supxrgelem  45911  supxrge  45912  xralrple2  45928  infxr  45940  infxrunb2  45941  xrralrecnnle  45956  xrralrecnnge  45963  supxrunb3  45972  supxrleubrnmpt  45978  infleinf2  45986  unb2ltle  45987  rexabslelem  45990  suprleubrnmpt  45994  uzub  46003  supminfrnmpt  46017  supxrleubrnmptf  46023  infxrgelbrnmpt  46026  infrpgernmpt  46037  monoordxr  46054  monoord2xr  46056  caucvgbf  46061  cvgcaule  46063  iccshift  46092  iooshift  46096  iooiinicc  46116  iooiinioc  46130  fsummulc1f  46145  fsumf1of  46148  fsumreclf  46150  fsumlessf  46151  fmul01  46154  fmuldfeqlem1  46156  fmuldfeq  46157  fmul01lt1lem1  46158  fmul01lt1lem2  46159  fprodexp  46168  mccl  46172  fprodcnlem  46173  fprodcn  46174  climmulf  46178  climexp  46179  climsuse  46182  climrecf  46183  climinff  46185  climaddf  46189  mullimc  46190  islptre  46193  climf  46196  mullimcf  46197  rexlim2d  46199  idlimc  46200  limcperiod  46202  limcrecl  46203  islpcn  46211  limsupre  46213  limcleqr  46216  addlimc  46220  limclner  46223  climsubmpt  46232  climreclf  46236  climf2  46238  climeldmeqmpt  46240  clim2f2  46242  climfveqmpt  46243  fnlimfvre  46246  allbutfifvre  46247  climleltrp  46248  fnlimf  46250  fnlimabslt  46251  climfveqf  46252  climfveqmpt3  46254  climeldmeqf  46255  climeqf  46260  climeldmeqmpt3  46261  limsuppnfd  46274  limsupub  46276  climinf2lem  46278  climinf2  46279  limsuppnf  46283  limsupubuz  46285  climinf2mpt  46286  climinfmpt  46287  climinf3  46288  limsupmnflem  46292  limsupequz  46295  limsupre2  46297  limsupmnfuzlem  46298  limsupequzmptf  46303  limsupre3  46305  limsupre3uzlem  46307  limsupreuzmpt  46311  climisp  46318  lmbr3  46319  climrescn  46320  climxrrelem  46321  climxrre  46322  limsupub2  46384  liminflbuz2  46387  xlimmnfvlem2  46405  xlimmnfv  46406  xlimpnfvlem2  46409  xlimpnfv  46410  xlimmnfmpt  46415  xlimpnfmpt  46416  climxlim2lem  46417  cncficcgt0  46460  cncfioobd  46469  fprodsubrecnncnvlem  46479  fprodaddrecnncnvlem  46481  dvmptmulf  46509  dvnmul  46515  dvmptfprodlem  46516  dvmptfprod  46517  dvnprodlem1  46518  dvnprodlem2  46519  iblsplitf  46542  itgperiod  46553  stoweidlem3  46575  stoweidlem26  46598  stoweidlem27  46599  stoweidlem29  46601  stoweidlem31  46603  stoweidlem34  46606  stoweidlem35  46607  stoweidlem36  46608  stoweidlem39  46611  stoweidlem42  46614  stoweidlem43  46615  stoweidlem44  46616  stoweidlem46  46618  stoweidlem48  46620  stoweidlem49  46621  stoweidlem51  46623  stoweidlem52  46624  stoweidlem53  46625  stoweidlem54  46626  stoweidlem55  46627  stoweidlem56  46628  stoweidlem57  46629  stoweidlem58  46630  stoweidlem59  46631  stoweidlem60  46632  stoweidlem61  46633  stoweidlem62  46634  stoweid  46635  wallispilem3  46639  stirlinglem13  46658  stirling  46661  fourierdlem16  46695  fourierdlem21  46700  fourierdlem22  46701  fourierdlem31  46710  fourierdlem39  46718  fourierdlem48  46726  fourierdlem51  46729  fourierdlem68  46746  fourierdlem71  46749  fourierdlem73  46751  fourierdlem80  46758  fourierdlem81  46759  fourierdlem86  46764  fourierdlem87  46765  fourierdlem93  46771  fourierdlem94  46772  fourierdlem103  46781  fourierdlem104  46782  fourierdlem112  46790  fourierdlem113  46791  elaa2  46806  etransclem32  46838  salexct  46906  sge0revalmpt  46950  sge0f1o  46954  sge0lefi  46970  sge0resplit  46978  sge0lempt  46982  sge0iunmptlemre  46987  sge0fodjrnlem  46988  sge0iunmpt  46990  sge0ltfirpmpt2  46998  sge0isum  46999  sge0xp  47001  sge0isummpt2  47004  sge0xadd  47007  sge0pnffsumgt  47014  sge0gtfsumgt  47015  sge0uzfsumgt  47016  sge0reuz  47019  sge0reuzb  47020  iundjiun  47032  meadjiun  47038  ismeannd  47039  voliunsge0lem  47044  meaiunincf  47055  meaiuninc3v  47056  meaiuninc3  47057  meaiininc  47059  caragenfiiuncl  47087  omeiunltfirp  47091  ovnsubaddlem2  47143  hoidmvval0  47159  hoidmvlelem1  47167  hoidmvlelem3  47169  hoidmvlelem5  47171  ovnlecvr2  47182  hspdifhsp  47188  hoiqssbllem2  47195  hoiqssbllem3  47196  hspmbllem2  47199  opnvonmbllem2  47205  hoimbl2  47237  vonhoire  47244  iinhoiicc  47246  iunhoiioolem  47247  iunhoiioo  47248  vonioo  47254  vonicc  47257  vonn0ioo2  47262  vonn0icc2  47264  salpreimagelt  47279  salpreimalegt  47281  pimincfltioc  47288  pimdecfgtioo  47289  pimincfltioo  47290  preimageiingt  47292  preimaleiinlt  47293  salpreimagtge  47297  salpreimaltle  47298  salpreimalelt  47301  salpreimagtlt  47302  incsmflem  47313  issmflelem  47316  issmfle  47317  smfconst  47321  issmfgtlem  47327  issmfgt  47328  smfaddlem2  47336  smfadd  47337  decsmflem  47338  decsmf  47339  issmfgelem  47341  issmfge  47342  smflimlem2  47344  smflim  47349  smfresal  47360  smfrec  47361  smfmullem4  47366  smfmul  47367  smfpimcc  47380  smflimmpt  47382  smfsuplem1  47383  smfsupmpt  47387  smfsupxr  47388  smfinflem  47389  smfinfmpt  47391  smflimsuplem5  47396  smflimsuplem7  47398  smflimsuplem8  47399  smflimsupmpt  47401  smfliminflem  47402  smfliminfmpt  47404  smfpimne2  47412  fsupdm  47414  smfsupdmmbllem  47416  finfdm  47418  smfinfdmmbllem  47420  or2expropbilem2  47625  or2expropbi  47626  cfsetsnfsetf  47650  2reu8i  47705  nfdfat  47719  iccelpart  48037  ichnfim  48068  ich2exprop  48075  ichreuopeq  48077  sprsymrelfo  48101  reupr  48126  reuopreuprim  48130  2zrngmmgm  48872  cbvmpox2  48967  ovmpordxf  48970  1arymaptfo  49274  2arymaptfo  49285  iinfssclem3  49685  iinfssc  49686  iinfsubc  49687  setrec1  50320  pgindnf  50345  aacllem  50430