Theorem nfan 1906

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

Syntax hints:   ∧ wa 396  ⊤wtru 1548  Ⅎwnf 1790

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791

This theorem is referenced by:  nfnan  1907  nf3an  1908  hban  2311  nfeqf  2389  nfald2  2453  2ax6elem  2478  nfsb4t  2507  nfeu1  2593  eupicka  2638  mopick2  2641  2mo  2652  nfabd2  2925  2ralbida  3263  r19.12  3289  reean  3290  ralcom2  3342  cbvrmow  3370  nfrmow  3374  nfreuw  3375  cbvreu  3384  cbvrabw  3427  cbvrabwOLD  3428  nfrabw  3429  cbvrab  3431  ceqsex2  3484  vtocl2gafOLD  3526  vtocl3gaf  3527  spc2ed  3546  rspce  3556  eqvincf  3595  elrabf  3633  elrab3t  3635  rexab2  3647  morex  3667  reu2  3673  rmo3f  3682  reu2eqd  3684  sbc2iegf  3804  reu8nf  3816  rmo2  3826  rmo3  3828  csbiebt  3867  csbie2t  3876  cbvrabcsfw  3879  cbvreucsf  3882  cbvrabcsf  3883  nfdif  4067  nfin  4160  reusngf  4613  rexreusng  4618  reuprg0  4641  rabsnifsb  4661  nfop  4827  nfopd  4828  eluniab  4859  iuneqconst  4940  cbvopab  5151  cbvopab1  5153  cbvopab1g  5154  cbvopab2  5155  cbvopab1s  5156  mpteq12f  5164  nfmpt  5177  cbvmptf  5179  cbvmptfg  5180  axrep3  5210  axrep4OLD  5213  axrep5  5214  reusv2lem3  5336  axprlem4OLD  5366  axprlem5OLD  5367  nfpo  5539  nfso  5540  nffr  5598  nfwe  5600  nfxp  5658  opeliunxp  5692  opeliun2xp  5693  nfco  5814  elrnmpt1  5909  nfimad  6028  reuop  6251  iota2  6481  nffun  6515  imadif  6576  nffn  6591  nff  6658  nff1  6728  nffo  6745  nff1o  6772  nffvd  6846  fv3  6852  funimassd  6900  fvmptdf  6949  fompt  7066  f1ossf1o  7077  fmptco  7078  fsnex  7234  nfiso  7273  nfriotadw  7328  cbvriotaw  7329  nfriotad  7331  cbvriota  7333  riota2df  7343  riota5f  7348  oprabv  7423  nfoprab  7427  mpoeq123  7435  nfmpo  7445  cbvoprab1  7450  cbvoprab2  7451  cbvoprab12  7452  cbvoprab3  7454  cbvmpox  7456  ovmpodxf  7513  elovmporab  7609  elovmporab1w  7610  elovmporab1  7611  onminex  7752  fiun  7892  f1iun  7893  opabex3d  7914  opabex3rd  7915  opabex3  7916  dfoprab4f  8005  fmpox  8016  opeliunxp2f  8157  nffrecs  8230  frrlem4  8236  tfr3  8335  tz7.49  8381  naddsuc2  8634  erovlem  8757  nfixpw  8861  nfixp  8862  nfixp1  8863  xpf1o  9074  nneneq  9137  ac6sfi  9191  nfoi  9426  wdom2d  9492  infpssrlem4  10226  hsmexlem2  10347  hsmexlem4  10349  domtriomlem  10362  axdc3lem2  10371  axdc4lem  10375  zorn2lem4  10419  zorn2lem5  10420  konigthlem  10489  axextnd  10512  axrepndlem2  10514  axrepnd  10515  axunnd  10517  axpowndlem2  10519  axpowndlem4  10521  axpownd  10522  axregndlem2  10524  axregnd  10525  axinfndlem1  10526  axinfnd  10527  zfcndrep  10535  zfcndinf  10539  dedekind  11307  dedekindle  11308  fsuppmapnn0fiublem  13950  fsuppmapnn0fiub  13951  fsuppmapnn0fiubex  13952  reuccatpfxs1  14707  nfsum1  15650  nfsum  15651  fsumclf  15698  fsumsplitf  15702  fsumsplit1  15705  fsum2dlem  15730  fsum00  15759  nfcprod1  15871  nfcprod  15872  fprod2dlem  15943  fprodsplitf  15951  fprodsplit1f  15953  fprodle  15959  lcmfunsnlem1  16604  lcmfunsnlem2lem1  16605  lcmfunsnlem2  16607  mreexexd  17612  acsmapd  18518  gsum2d2lem  19946  dprd2d2  20019  gsummoncoe1  22301  gsummatr01lem4  22648  cpmatmcllem  22708  cayleyhamilton1  22882  neiptopnei  23122  neiptopreu  23123  neitr  23170  iunconnlem  23417  iunconn  23418  ptcnplem  23611  ptcnp  23612  xkocnv  23804  isfildlem  23847  utopsnneiplem  24237  isucn2  24268  cfilucfil  24549  restmetu  24560  ovolfiniun  25493  ovoliunlem3  25496  ovoliunnul  25499  volfiniun  25539  itg2splitlem  25740  itg2split  25741  isibl2  25758  nfitg  25767  cbvitg  25768  limciun  25886  2sqmo  27425  2sqreulem4  27442  bdaypw2n0bndlem  28480  istrkg2ld  28553  chirred  32491  sbc2iedf  32559  rspc2daf  32560  opreu2reuALT  32571  mo5f  32583  foresf1o  32599  iinabrex  32665  cbvdisjf  32667  disjabrex  32678  disjabrexf  32679  funimass4f  32736  2ndresdju  32748  fmptcof2  32756  fcomptf  32757  acunirnmpt2  32759  acunirnmpt2f  32760  aciunf1lem  32761  funcnv4mpt  32767  fnpreimac  32769  f1od2  32818  fpwrelmap  32832  xrofsup  32866  nn0min  32920  fprodex01  32924  fsumiunle  32928  prodindf  32948  suppgsumssiun  33160  isarchiofld  33287  elrgspnsubrunlem2  33336  nsgqusf1olem1  33503  nsgqusf1olem3  33505  elrspunidl  33518  deg1prod  33673  mplvrpmga  33736  esplyfval1  33764  vieta  33771  fedgmullem2  33821  irngnzply1  33882  reff  34030  locfinreflem  34031  cmpcref  34041  zarclsiin  34062  zarcmplem  34072  ordtconnlem1  34115  esumcl  34221  gsumesum  34250  esumlub  34251  esumcst  34254  esumrnmpt2  34259  esumfzf  34260  esumfsup  34261  hasheuni  34276  esumcvg  34277  esumgect  34281  esumcvgre  34282  esum2dlem  34283  esum2d  34284  esumiun  34285  ldsysgenld  34351  sigapildsyslem  34352  sigapildsys  34353  ldgenpisyslem1  34354  measvunilem  34403  measvunilem0  34404  measvuni  34405  measinblem  34411  voliune  34420  volfiniune  34421  volmeas  34422  oms0  34488  omssubadd  34491  eulerpartlemgvv  34567  dstrvprob  34663  breprexplema  34821  bnj919  34957  bnj1146  34980  bnj1379  35019  bnj849  35114  bnj916  35122  bnj964  35132  bnj1014  35150  bnj1123  35175  bnj1228  35200  bnj1307  35212  bnj1321  35216  bnj1398  35223  bnj1408  35225  bnj1444  35232  bnj1445  35233  bnj1446  35234  bnj1449  35237  bnj1467  35243  bnj1463  35244  bnj1489  35245  bnj1491  35246  bnj1312  35247  bnj1525  35258  dvelimalcased  35264  dvelimexcased  35266  fineqvrep  35305  cvmcov  35492  iota5f  35953  axextdist  36026  axextbdist  36027  nfwlim  36049  finminlem  36547  axtcond  36707  bj-dvelimdv  37205  bj-axreprepsep  37429  bj-opabco  37549  isbasisrelowllem1  37718  isbasisrelowllem2  37719  fvineqsneu  37774  fvineqsneq  37775  wl-cbvalnaed  37904  wl-2sb6d  37930  wl-sbalnae  37934  wl-mo2tf  37943  wl-eutf  37945  phpreu  37972  poimirlem26  38014  poimirlem27  38015  heicant  38023  mbfposadd  38035  ftc1anclem5  38065  indexdom  38102  filbcmb  38108  sdclem2  38110  sdclem1  38111  fdc1  38114  riotasv2d  39450  riotasv2s  39451  nfded2  39461  glbconxN  39871  pmapglb2xN  40265  cdlemefs32sn1aw  40907  mzpsubmpt  43193  mzpexpmpt  43195  eq0rabdioph  43226  eqrabdioph  43227  setindtr  43470  unielss  43664  nadd1suc  43838  ss2iundf  44104  scottabf  44685  mnuprdlem4  44720  ismnushort  44746  binomcxplemnotnn0  44801  iunconnlem2  45379  nfrelp  45394  modelaxreplem3  45425  modelaxrep  45426  permaxrep  45451  elunif  45465  rspcegf  45472  fnchoice  45478  refsumcn  45479  rfcnnnub  45485  uzwo4  45502  fiiuncl  45514  cbvmpo2  45545  cbvmpo1  45546  iinssiin  45577  disjf1  45631  disjrnmpt2  45636  disjf1o  45639  disjinfi  45640  choicefi  45647  axccdom  45668  dmrelrnrel  45672  axccd  45674  rnmptbddlem  45689  rnmptbd2lem  45693  infnsuprnmpt  45695  rnmptbdlem  45700  rnmptssbi  45705  upbdrech  45754  ssfiunibd  45758  supxrgere  45779  supxrgelem  45783  supxrge  45784  xralrple2  45800  infxr  45812  infxrunb2  45813  xrralrecnnle  45828  xrralrecnnge  45835  supxrunb3  45844  supxrleubrnmpt  45850  infleinf2  45858  unb2ltle  45859  rexabslelem  45862  suprleubrnmpt  45866  uzub  45875  supminfrnmpt  45889  supxrleubrnmptf  45895  infxrgelbrnmpt  45898  infrpgernmpt  45909  monoordxr  45926  monoord2xr  45928  caucvgbf  45933  cvgcaule  45935  iccshift  45964  iooshift  45968  iooiinicc  45988  iooiinioc  46002  fsummulc1f  46017  fsumf1of  46020  fsumreclf  46022  fsumlessf  46023  fmul01  46026  fmuldfeqlem1  46028  fmuldfeq  46029  fmul01lt1lem1  46030  fmul01lt1lem2  46031  fprodexp  46040  mccl  46044  fprodcnlem  46045  fprodcn  46046  climmulf  46050  climexp  46051  climsuse  46054  climrecf  46055  climinff  46057  climaddf  46061  mullimc  46062  islptre  46065  climf  46068  mullimcf  46069  rexlim2d  46071  idlimc  46072  limcperiod  46074  limcrecl  46075  islpcn  46083  limsupre  46085  limcleqr  46088  addlimc  46092  limclner  46095  climsubmpt  46104  climreclf  46108  climf2  46110  climeldmeqmpt  46112  clim2f2  46114  climfveqmpt  46115  fnlimfvre  46118  allbutfifvre  46119  climleltrp  46120  fnlimf  46122  fnlimabslt  46123  climfveqf  46124  climfveqmpt3  46126  climeldmeqf  46127  climeqf  46132  climeldmeqmpt3  46133  limsuppnfd  46146  limsupub  46148  climinf2lem  46150  climinf2  46151  limsuppnf  46155  limsupubuz  46157  climinf2mpt  46158  climinfmpt  46159  climinf3  46160  limsupmnflem  46164  limsupequz  46167  limsupre2  46169  limsupmnfuzlem  46170  limsupequzmptf  46175  limsupre3  46177  limsupre3uzlem  46179  limsupreuzmpt  46183  climisp  46190  lmbr3  46191  climrescn  46192  climxrrelem  46193  climxrre  46194  limsupub2  46256  liminflbuz2  46259  xlimmnfvlem2  46277  xlimmnfv  46278  xlimpnfvlem2  46281  xlimpnfv  46282  xlimmnfmpt  46287  xlimpnfmpt  46288  climxlim2lem  46289  cncficcgt0  46332  cncfioobd  46341  fprodsubrecnncnvlem  46351  fprodaddrecnncnvlem  46353  dvmptmulf  46381  dvnmul  46387  dvmptfprodlem  46388  dvmptfprod  46389  dvnprodlem1  46390  dvnprodlem2  46391  iblsplitf  46414  itgperiod  46425  stoweidlem3  46447  stoweidlem26  46470  stoweidlem27  46471  stoweidlem29  46473  stoweidlem31  46475  stoweidlem34  46478  stoweidlem35  46479  stoweidlem36  46480  stoweidlem39  46483  stoweidlem42  46486  stoweidlem43  46487  stoweidlem44  46488  stoweidlem46  46490  stoweidlem48  46492  stoweidlem49  46493  stoweidlem51  46495  stoweidlem52  46496  stoweidlem53  46497  stoweidlem54  46498  stoweidlem55  46499  stoweidlem56  46500  stoweidlem57  46501  stoweidlem58  46502  stoweidlem59  46503  stoweidlem60  46504  stoweidlem61  46505  stoweidlem62  46506  stoweid  46507  wallispilem3  46511  stirlinglem13  46530  stirling  46533  fourierdlem16  46567  fourierdlem21  46572  fourierdlem22  46573  fourierdlem31  46582  fourierdlem39  46590  fourierdlem48  46598  fourierdlem51  46601  fourierdlem68  46618  fourierdlem71  46621  fourierdlem73  46623  fourierdlem80  46630  fourierdlem81  46631  fourierdlem86  46636  fourierdlem87  46637  fourierdlem93  46643  fourierdlem94  46644  fourierdlem103  46653  fourierdlem104  46654  fourierdlem112  46662  fourierdlem113  46663  elaa2  46678  etransclem32  46710  salexct  46778  sge0revalmpt  46822  sge0f1o  46826  sge0lefi  46842  sge0resplit  46850  sge0lempt  46854  sge0iunmptlemre  46859  sge0fodjrnlem  46860  sge0iunmpt  46862  sge0ltfirpmpt2  46870  sge0isum  46871  sge0xp  46873  sge0isummpt2  46876  sge0xadd  46879  sge0pnffsumgt  46886  sge0gtfsumgt  46887  sge0uzfsumgt  46888  sge0reuz  46891  sge0reuzb  46892  iundjiun  46904  meadjiun  46910  ismeannd  46911  voliunsge0lem  46916  meaiunincf  46927  meaiuninc3v  46928  meaiuninc3  46929  meaiininc  46931  caragenfiiuncl  46959  omeiunltfirp  46963  ovnsubaddlem2  47015  hoidmvval0  47031  hoidmvlelem1  47039  hoidmvlelem3  47041  hoidmvlelem5  47043  ovnlecvr2  47054  hspdifhsp  47060  hoiqssbllem2  47067  hoiqssbllem3  47068  hspmbllem2  47071  opnvonmbllem2  47077  hoimbl2  47109  vonhoire  47116  iinhoiicc  47118  iunhoiioolem  47119  iunhoiioo  47120  vonioo  47126  vonicc  47129  vonn0ioo2  47134  vonn0icc2  47136  salpreimagelt  47151  salpreimalegt  47153  pimincfltioc  47160  pimdecfgtioo  47161  pimincfltioo  47162  preimageiingt  47164  preimaleiinlt  47165  salpreimagtge  47169  salpreimaltle  47170  salpreimalelt  47173  salpreimagtlt  47174  incsmflem  47185  issmflelem  47188  issmfle  47189  smfconst  47193  issmfgtlem  47199  issmfgt  47200  smfaddlem2  47208  smfadd  47209  decsmflem  47210  decsmf  47211  issmfgelem  47213  issmfge  47214  smflimlem2  47216  smflim  47221  smfresal  47232  smfrec  47233  smfmullem4  47238  smfmul  47239  smfpimcc  47252  smflimmpt  47254  smfsuplem1  47255  smfsupmpt  47259  smfsupxr  47260  smfinflem  47261  smfinfmpt  47263  smflimsuplem5  47268  smflimsuplem7  47270  smflimsuplem8  47271  smflimsupmpt  47273  smfliminflem  47274  smfliminfmpt  47276  smfpimne2  47284  fsupdm  47286  smfsupdmmbllem  47288  finfdm  47290  smfinfdmmbllem  47292  or2expropbilem2  47497  or2expropbi  47498  cfsetsnfsetf  47522  2reu8i  47577  nfdfat  47591  iccelpart  47909  ichnfim  47940  ich2exprop  47947  ichreuopeq  47949  sprsymrelfo  47973  reupr  47998  reuopreuprim  48002  2zrngmmgm  48744  cbvmpox2  48828  ovmpordxf  48831  1arymaptfo  49135  2arymaptfo  49146  iinfssclem3  49547  iinfssc  49548  iinfsubc  49549  setrec1  50182  pgindnf  50207  aacllem  50292