Theorem nfan 1894

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

Syntax hints:   ∧ wa 394  ⊤wtru 1534  Ⅎwnf 1777

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-nf 1778

This theorem is referenced by:  nfnan  1895  nf3an  1896  hban  2289  nfeqf  2374  nfald2  2438  2ax6elem  2463  nfsb4t  2492  nfeu1ALT  2577  eupicka  2622  mopick2  2625  2mo  2636  clelabOLD  2872  nfabd2  2918  2ralbida  3270  r19.12  3301  r19.12OLD  3302  reean  3303  ralcom2  3360  cbvrmow  3392  nfrmow  3396  nfreuw  3397  cbvreuwOLD  3398  cbvreu  3410  cbvrabw  3455  nfrabw  3456  cbvrab  3460  ceqsex2  3519  vtocl2gafOLD  3559  vtocl3gaf  3560  spc2ed  3585  rspce  3595  eqvincf  3633  elrabf  3675  elrab3t  3678  rexab2  3691  morex  3711  reu2  3717  rmo3f  3726  reu2eqd  3728  sbc2iegf  3855  reu8nf  3867  rmo2  3877  rmo3  3879  csbiebt  3919  csbie2t  3930  cbvrabcsfw  3933  cbvreucsf  3936  cbvrabcsf  3937  nfdif  4121  nfin  4214  reusngf  4678  rexreusng  4685  reuprg0  4708  rabsnifsb  4728  nfop  4891  nfopd  4892  eluniab  4923  iuneqconst  5008  cbvopab  5221  cbvopab1  5224  cbvopab1g  5225  cbvopab2  5226  cbvopab1s  5227  mpteq12f  5237  nfmpt  5256  cbvmptf  5258  cbvmptfg  5259  axrep3  5290  axrep4  5291  axrep5  5292  reusv2lem3  5400  axprlem4  5426  axprlem5  5427  nfpo  5595  nfso  5596  nffr  5652  nfwe  5654  nfxp  5711  opeliunxp  5745  nfco  5868  elrnmpt1  5960  nfimad  6073  reuop  6299  iota2  6538  nffun  6577  imadif  6638  nffn  6654  nff  6719  nff1  6791  nffo  6809  nff1o  6836  nffvd  6908  fv3  6914  funimassd  6964  fvmptdf  7010  fompt  7127  f1ossf1o  7137  fmptco  7138  fsnex  7292  nfiso  7329  nfriotadw  7383  cbvriotaw  7384  nfriotad  7387  cbvriota  7389  riota2df  7399  riota5f  7404  oprabv  7480  nfoprab  7484  mpoeq123  7492  nfmpo  7502  cbvoprab1  7507  cbvoprab2  7508  cbvoprab12  7509  cbvoprab3  7511  cbvmpox  7513  ovmpodxf  7571  elovmporab  7667  elovmporab1w  7668  elovmporab1  7669  onminex  7806  peano5OLD  7901  fiun  7947  f1iun  7948  opabex3d  7970  opabex3rd  7971  opabex3  7972  dfoprab4f  8061  fmpox  8072  opeliunxp2f  8216  nffrecs  8289  frrlem4  8295  nfwrecsOLD  8323  wfrlem4OLD  8333  tfr3  8420  tz7.49  8466  erovlem  8832  nfixpw  8935  nfixp  8936  nfixp1  8937  xpf1o  9164  nneneq  9234  nneneqOLD  9246  ac6sfi  9312  nfoi  9539  wdom2d  9605  infpssrlem4  10331  hsmexlem2  10452  hsmexlem4  10454  domtriomlem  10467  axdc3lem2  10476  axdc4lem  10480  zorn2lem4  10524  zorn2lem5  10525  konigthlem  10593  axextnd  10616  axrepndlem2  10618  axrepnd  10619  axunnd  10621  axpowndlem2  10623  axpowndlem4  10625  axpownd  10626  axregndlem2  10628  axregnd  10629  axinfndlem1  10630  axinfnd  10631  zfcndrep  10639  zfcndinf  10643  dedekind  11409  dedekindle  11410  fsuppmapnn0fiublem  13991  fsuppmapnn0fiub  13992  fsuppmapnn0fiubex  13993  reuccatpfxs1  14733  nfsum1  15672  nfsum  15673  fsumclf  15720  fsumsplitf  15724  fsumsplit1  15727  fsum2dlem  15752  fsum00  15780  nfcprod1  15890  nfcprod  15891  fprod2dlem  15960  fprodsplitf  15968  fprodsplit1f  15970  fprodle  15976  lcmfunsnlem1  16611  lcmfunsnlem2lem1  16612  lcmfunsnlem2  16614  mreexexd  17631  acsmapd  18549  gsum2d2lem  19940  dprd2d2  20013  gsummoncoe1  22252  gsummatr01lem4  22604  cpmatmcllem  22664  cayleyhamilton1  22838  neiptopnei  23080  neiptopreu  23081  neitr  23128  iunconnlem  23375  iunconn  23376  ptcnplem  23569  ptcnp  23570  xkocnv  23762  isfildlem  23805  utopsnneiplem  24196  isucn2  24228  cfilucfil  24512  restmetu  24523  ovolfiniun  25474  ovoliunlem3  25477  ovoliunnul  25480  volfiniun  25520  itg2splitlem  25722  itg2split  25723  isibl2  25740  nfitg  25748  cbvitg  25749  limciun  25867  2sqmo  27415  2sqreulem4  27432  istrkg2ld  28336  chirred  32277  sbc2iedf  32343  rspc2daf  32344  opreu2reuALT  32353  mo5f  32365  foresf1o  32378  iinabrex  32438  cbvdisjf  32440  disjabrex  32451  disjabrexf  32452  funimass4f  32503  2ndresdju  32516  fmptcof2  32524  fcomptf  32525  acunirnmpt2  32527  acunirnmpt2f  32528  aciunf1lem  32529  funcnv4mpt  32536  fnpreimac  32538  cnvoprabOLD  32584  f1od2  32585  fpwrelmap  32597  xrofsup  32619  nn0min  32668  fprodex01  32673  fsumiunle  32677  isarchiofld  33131  nsgqusf1olem1  33225  nsgqusf1olem3  33227  elrspunidl  33240  fedgmullem2  33459  irngnzply1  33500  reff  33571  locfinreflem  33572  cmpcref  33582  zarclsiin  33603  zarcmplem  33613  ordtconnlem1  33656  prodindf  33773  esumcl  33780  gsumesum  33809  esumlub  33810  esumcst  33813  esumrnmpt2  33818  esumfzf  33819  esumfsup  33820  hasheuni  33835  esumcvg  33836  esumgect  33840  esumcvgre  33841  esum2dlem  33842  esum2d  33843  esumiun  33844  ldsysgenld  33910  sigapildsyslem  33911  sigapildsys  33912  ldgenpisyslem1  33913  measvunilem  33962  measvunilem0  33963  measvuni  33964  measinblem  33970  voliune  33979  volfiniune  33980  volmeas  33981  oms0  34048  omssubadd  34051  eulerpartlemgvv  34127  dstrvprob  34222  breprexplema  34393  bnj919  34529  bnj1146  34553  bnj1379  34592  bnj849  34687  bnj916  34695  bnj964  34705  bnj1014  34723  bnj1123  34748  bnj1228  34773  bnj1307  34785  bnj1321  34789  bnj1398  34796  bnj1408  34798  bnj1444  34805  bnj1445  34806  bnj1446  34807  bnj1449  34810  bnj1467  34816  bnj1463  34817  bnj1489  34818  bnj1491  34819  bnj1312  34820  bnj1525  34831  fineqvrep  34846  cvmcov  35004  iota5f  35449  axextdist  35526  axextbdist  35527  nfwlim  35549  finminlem  35933  bj-dvelimdv  36459  bj-opabco  36798  isbasisrelowllem1  36965  isbasisrelowllem2  36966  fvineqsneu  37021  fvineqsneq  37022  wl-cbvalnaed  37130  wl-2sb6d  37156  wl-sbalnae  37160  wl-mo2tf  37169  wl-eutf  37171  wl-ax11-lem3  37185  phpreu  37208  poimirlem26  37250  poimirlem27  37251  heicant  37259  mbfposadd  37271  ftc1anclem5  37301  indexdom  37338  filbcmb  37344  sdclem2  37346  sdclem1  37347  fdc1  37350  riotasv2d  38559  riotasv2s  38560  nfded2  38570  glbconxN  38981  pmapglb2xN  39375  cdlemefs32sn1aw  40017  mzpsubmpt  42305  mzpexpmpt  42307  eq0rabdioph  42338  eqrabdioph  42339  setindtr  42587  unielss  42788  nadd1suc  42963  naddsuc2  42964  ss2iundf  43231  scottabf  43819  mnuprdlem4  43854  ismnushort  43880  binomcxplemnotnn0  43935  iunconnlem2  44516  elunif  44520  rspcegf  44527  fnchoice  44533  refsumcn  44534  rfcnnnub  44540  uzwo4  44559  fiiuncl  44571  cbvmpo2  44603  cbvmpo1  44604  iinssiin  44635  disjf1  44695  disjrnmpt2  44700  disjf1o  44703  disjinfi  44704  choicefi  44712  axccdom  44734  dmrelrnrel  44738  axccd  44741  rnmptbddlem  44758  rnmptbd2lem  44762  infnsuprnmpt  44764  rnmptbdlem  44769  rnmptssbi  44775  upbdrech  44825  ssfiunibd  44829  supxrgere  44853  supxrgelem  44857  supxrge  44858  xralrple2  44874  infxr  44887  infxrunb2  44888  xrralrecnnle  44903  xrralrecnnge  44910  supxrunb3  44919  supxrleubrnmpt  44926  infleinf2  44934  unb2ltle  44935  rexabslelem  44938  suprleubrnmpt  44942  uzub  44951  supminfrnmpt  44965  supxrleubrnmptf  44971  infxrgelbrnmpt  44974  infrpgernmpt  44985  monoordxr  45003  monoord2xr  45005  caucvgbf  45010  cvgcaule  45012  iccshift  45041  iooshift  45045  iooiinicc  45065  iooiinioc  45079  fsummulc1f  45097  fsumf1of  45100  fsumreclf  45102  fsumlessf  45103  fmul01  45106  fmuldfeqlem1  45108  fmuldfeq  45109  fmul01lt1lem1  45110  fmul01lt1lem2  45111  fprodexp  45120  mccl  45124  fprodcnlem  45125  fprodcn  45126  climmulf  45130  climexp  45131  climsuse  45134  climrecf  45135  climinff  45137  climaddf  45141  mullimc  45142  islptre  45145  climf  45148  mullimcf  45149  rexlim2d  45151  idlimc  45152  limcperiod  45154  limcrecl  45155  islpcn  45165  limsupre  45167  limcleqr  45170  addlimc  45174  limclner  45177  climsubmpt  45186  climreclf  45190  climf2  45192  climeldmeqmpt  45194  clim2f2  45196  climfveqmpt  45197  fnlimfvre  45200  allbutfifvre  45201  climleltrp  45202  fnlimf  45204  fnlimabslt  45205  climfveqf  45206  climfveqmpt3  45208  climeldmeqf  45209  climeqf  45214  climeldmeqmpt3  45215  limsuppnfd  45228  limsupub  45230  climinf2lem  45232  climinf2  45233  limsuppnf  45237  limsupubuz  45239  climinf2mpt  45240  climinfmpt  45241  climinf3  45242  limsupmnflem  45246  limsupequz  45249  limsupre2  45251  limsupmnfuzlem  45252  limsupequzmptf  45257  limsupre3  45259  limsupre3uzlem  45261  limsupreuzmpt  45265  climisp  45272  lmbr3  45273  climrescn  45274  climxrrelem  45275  climxrre  45276  limsupub2  45338  liminflbuz2  45341  xlimmnfvlem2  45359  xlimmnfv  45360  xlimpnfvlem2  45363  xlimpnfv  45364  xlimmnfmpt  45369  xlimpnfmpt  45370  climxlim2lem  45371  cncficcgt0  45414  cncfioobd  45423  fprodsubrecnncnvlem  45433  fprodaddrecnncnvlem  45435  dvmptmulf  45463  dvnmul  45469  dvmptfprodlem  45470  dvmptfprod  45471  dvnprodlem1  45472  dvnprodlem2  45473  iblsplitf  45496  itgperiod  45507  stoweidlem3  45529  stoweidlem26  45552  stoweidlem27  45553  stoweidlem29  45555  stoweidlem31  45557  stoweidlem34  45560  stoweidlem35  45561  stoweidlem36  45562  stoweidlem39  45565  stoweidlem42  45568  stoweidlem43  45569  stoweidlem44  45570  stoweidlem46  45572  stoweidlem48  45574  stoweidlem49  45575  stoweidlem51  45577  stoweidlem52  45578  stoweidlem53  45579  stoweidlem54  45580  stoweidlem55  45581  stoweidlem56  45582  stoweidlem57  45583  stoweidlem58  45584  stoweidlem59  45585  stoweidlem60  45586  stoweidlem61  45587  stoweidlem62  45588  stoweid  45589  wallispilem3  45593  stirlinglem13  45612  stirling  45615  fourierdlem16  45649  fourierdlem21  45654  fourierdlem22  45655  fourierdlem31  45664  fourierdlem39  45672  fourierdlem48  45680  fourierdlem51  45683  fourierdlem68  45700  fourierdlem71  45703  fourierdlem73  45705  fourierdlem80  45712  fourierdlem81  45713  fourierdlem86  45718  fourierdlem87  45719  fourierdlem93  45725  fourierdlem94  45726  fourierdlem103  45735  fourierdlem104  45736  fourierdlem112  45744  fourierdlem113  45745  elaa2  45760  etransclem32  45792  salexct  45860  sge0revalmpt  45904  sge0f1o  45908  sge0lefi  45924  sge0resplit  45932  sge0lempt  45936  sge0iunmptlemre  45941  sge0fodjrnlem  45942  sge0iunmpt  45944  sge0ltfirpmpt2  45952  sge0isum  45953  sge0xp  45955  sge0isummpt2  45958  sge0xadd  45961  sge0pnffsumgt  45968  sge0gtfsumgt  45969  sge0uzfsumgt  45970  sge0reuz  45973  sge0reuzb  45974  iundjiun  45986  meadjiun  45992  ismeannd  45993  voliunsge0lem  45998  meaiunincf  46009  meaiuninc3v  46010  meaiuninc3  46011  meaiininc  46013  caragenfiiuncl  46041  omeiunltfirp  46045  ovnsubaddlem2  46097  hoidmvval0  46113  hoidmvlelem1  46121  hoidmvlelem3  46123  hoidmvlelem5  46125  ovnlecvr2  46136  hspdifhsp  46142  hoiqssbllem2  46149  hoiqssbllem3  46150  hspmbllem2  46153  opnvonmbllem2  46159  hoimbl2  46191  vonhoire  46198  iinhoiicc  46200  iunhoiioolem  46201  iunhoiioo  46202  vonioo  46208  vonicc  46211  vonn0ioo2  46216  vonn0icc2  46218  salpreimagelt  46233  salpreimalegt  46235  pimincfltioc  46242  pimdecfgtioo  46243  pimincfltioo  46244  preimageiingt  46246  preimaleiinlt  46247  salpreimagtge  46251  salpreimaltle  46252  salpreimalelt  46255  salpreimagtlt  46256  incsmflem  46267  issmflelem  46270  issmfle  46271  smfconst  46275  issmfgtlem  46281  issmfgt  46282  smfaddlem2  46290  smfadd  46291  decsmflem  46292  decsmf  46293  issmfgelem  46295  issmfge  46296  smflimlem2  46298  smflim  46303  smfresal  46314  smfrec  46315  smfmullem4  46320  smfmul  46321  smfpimcc  46334  smflimmpt  46336  smfsuplem1  46337  smfsupmpt  46341  smfsupxr  46342  smfinflem  46343  smfinfmpt  46345  smflimsuplem5  46350  smflimsuplem7  46352  smflimsuplem8  46353  smflimsupmpt  46355  smfliminflem  46356  smfliminfmpt  46358  smfpimne2  46366  fsupdm  46368  smfsupdmmbllem  46370  finfdm  46372  smfinfdmmbllem  46374  or2expropbilem2  46553  or2expropbi  46554  cfsetsnfsetf  46578  2reu8i  46631  nfdfat  46645  iccelpart  46910  ichnfim  46941  ich2exprop  46948  ichreuopeq  46950  sprsymrelfo  46974  reupr  46999  reuopreuprim  47003  2zrngmmgm  47500  opeliun2xp  47582  cbvmpox2  47585  ovmpordxf  47588  1arymaptfo  47902  2arymaptfo  47913  setrec1  48308  pgindnf  48333  aacllem  48420