Theorem nfan 1896

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

Syntax hints:   ∧ wa 395  ⊤wtru 1537  Ⅎwnf 1779

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-nf 1780

This theorem is referenced by:  nfnan  1897  nf3an  1898  hban  2298  nfeqf  2383  nfald2  2447  2ax6elem  2472  nfsb4t  2501  nfeu1ALT  2586  eupicka  2631  mopick2  2634  2mo  2645  nfabd2  2926  2ralbida  3280  r19.12  3311  r19.12OLD  3312  reean  3313  ralcom2  3374  cbvrmow  3406  nfrmow  3410  nfreuw  3411  cbvreuwOLD  3412  cbvreu  3424  cbvrabw  3470  cbvrabwOLD  3471  nfrabw  3472  cbvrab  3476  ceqsex2  3534  vtocl2gafOLD  3579  vtocl3gaf  3580  spc2ed  3600  rspce  3610  eqvincf  3649  elrabf  3690  elrab3t  3693  rexab2  3707  morex  3727  reu2  3733  rmo3f  3742  reu2eqd  3744  sbc2iegf  3872  reu8nf  3885  rmo2  3895  rmo3  3897  csbiebt  3937  csbie2t  3948  cbvrabcsfw  3951  cbvreucsf  3954  cbvrabcsf  3955  nfdif  4138  nfin  4231  reusngf  4678  rexreusng  4683  reuprg0  4706  rabsnifsb  4726  nfop  4893  nfopd  4894  eluniab  4925  iuneqconst  5007  cbvopab  5219  cbvopab1  5222  cbvopab1g  5223  cbvopab2  5224  cbvopab1s  5225  mpteq12f  5235  nfmpt  5254  cbvmptf  5256  cbvmptfg  5257  axrep3  5288  axrep4OLD  5291  axrep5  5292  reusv2lem3  5405  axprlem4OLD  5434  axprlem5OLD  5435  nfpo  5602  nfso  5603  nffr  5661  nfwe  5663  nfxp  5721  opeliunxp  5755  nfco  5878  elrnmpt1  5973  nfimad  6088  reuop  6314  iota2  6551  nffun  6590  imadif  6651  nffn  6667  nff  6732  nff1  6802  nffo  6819  nff1o  6846  nffvd  6918  fv3  6924  funimassd  6974  fvmptdf  7021  fompt  7137  f1ossf1o  7147  fmptco  7148  fsnex  7302  nfiso  7341  nfriotadw  7395  cbvriotaw  7396  nfriotad  7398  cbvriota  7400  riota2df  7410  riota5f  7415  oprabv  7492  nfoprab  7496  mpoeq123  7504  nfmpo  7514  cbvoprab1  7519  cbvoprab2  7520  cbvoprab12  7521  cbvoprab3  7523  cbvmpox  7525  ovmpodxf  7582  elovmporab  7678  elovmporab1w  7679  elovmporab1  7680  onminex  7821  fiun  7965  f1iun  7966  opabex3d  7988  opabex3rd  7989  opabex3  7990  dfoprab4f  8079  fmpox  8090  opeliunxp2f  8233  nffrecs  8306  frrlem4  8312  nfwrecsOLD  8340  wfrlem4OLD  8350  tfr3  8437  tz7.49  8483  naddsuc2  8737  erovlem  8851  nfixpw  8954  nfixp  8955  nfixp1  8956  xpf1o  9177  nneneq  9243  nneneqOLD  9255  ac6sfi  9317  nfoi  9551  wdom2d  9617  infpssrlem4  10343  hsmexlem2  10464  hsmexlem4  10466  domtriomlem  10479  axdc3lem2  10488  axdc4lem  10492  zorn2lem4  10536  zorn2lem5  10537  konigthlem  10605  axextnd  10628  axrepndlem2  10630  axrepnd  10631  axunnd  10633  axpowndlem2  10635  axpowndlem4  10637  axpownd  10638  axregndlem2  10640  axregnd  10641  axinfndlem1  10642  axinfnd  10643  zfcndrep  10651  zfcndinf  10655  dedekind  11421  dedekindle  11422  fsuppmapnn0fiublem  14027  fsuppmapnn0fiub  14028  fsuppmapnn0fiubex  14029  reuccatpfxs1  14781  nfsum1  15722  nfsum  15723  fsumclf  15770  fsumsplitf  15774  fsumsplit1  15777  fsum2dlem  15802  fsum00  15830  nfcprod1  15940  nfcprod  15941  fprod2dlem  16012  fprodsplitf  16020  fprodsplit1f  16022  fprodle  16028  lcmfunsnlem1  16670  lcmfunsnlem2lem1  16671  lcmfunsnlem2  16673  mreexexd  17692  acsmapd  18611  gsum2d2lem  20005  dprd2d2  20078  gsummoncoe1  22327  gsummatr01lem4  22679  cpmatmcllem  22739  cayleyhamilton1  22913  neiptopnei  23155  neiptopreu  23156  neitr  23203  iunconnlem  23450  iunconn  23451  ptcnplem  23644  ptcnp  23645  xkocnv  23837  isfildlem  23880  utopsnneiplem  24271  isucn2  24303  cfilucfil  24587  restmetu  24598  ovolfiniun  25549  ovoliunlem3  25552  ovoliunnul  25555  volfiniun  25595  itg2splitlem  25797  itg2split  25798  isibl2  25815  nfitg  25824  cbvitg  25825  limciun  25943  2sqmo  27495  2sqreulem4  27512  istrkg2ld  28482  chirred  32423  sbc2iedf  32493  rspc2daf  32494  opreu2reuALT  32504  mo5f  32516  foresf1o  32531  iinabrex  32588  cbvdisjf  32590  disjabrex  32601  disjabrexf  32602  funimass4f  32653  2ndresdju  32665  fmptcof2  32673  fcomptf  32674  acunirnmpt2  32676  acunirnmpt2f  32677  aciunf1lem  32678  funcnv4mpt  32685  fnpreimac  32687  cnvoprabOLD  32737  f1od2  32738  fpwrelmap  32750  xrofsup  32777  nn0min  32826  fprodex01  32831  fsumiunle  32835  isarchiofld  33326  nsgqusf1olem1  33420  nsgqusf1olem3  33422  elrspunidl  33435  fedgmullem2  33657  irngnzply1  33705  reff  33799  locfinreflem  33800  cmpcref  33810  zarclsiin  33831  zarcmplem  33841  ordtconnlem1  33884  prodindf  34003  esumcl  34010  gsumesum  34039  esumlub  34040  esumcst  34043  esumrnmpt2  34048  esumfzf  34049  esumfsup  34050  hasheuni  34065  esumcvg  34066  esumgect  34070  esumcvgre  34071  esum2dlem  34072  esum2d  34073  esumiun  34074  ldsysgenld  34140  sigapildsyslem  34141  sigapildsys  34142  ldgenpisyslem1  34143  measvunilem  34192  measvunilem0  34193  measvuni  34194  measinblem  34200  voliune  34209  volfiniune  34210  volmeas  34211  oms0  34278  omssubadd  34281  eulerpartlemgvv  34357  dstrvprob  34452  breprexplema  34623  bnj919  34759  bnj1146  34783  bnj1379  34822  bnj849  34917  bnj916  34925  bnj964  34935  bnj1014  34953  bnj1123  34978  bnj1228  35003  bnj1307  35015  bnj1321  35019  bnj1398  35026  bnj1408  35028  bnj1444  35035  bnj1445  35036  bnj1446  35037  bnj1449  35040  bnj1467  35046  bnj1463  35047  bnj1489  35048  bnj1491  35049  bnj1312  35050  bnj1525  35061  dvelimalcased  35067  dvelimexcased  35069  fineqvrep  35087  cvmcov  35247  iota5f  35703  axextdist  35780  axextbdist  35781  nfwlim  35803  finminlem  36300  bj-dvelimdv  36833  bj-opabco  37170  isbasisrelowllem1  37337  isbasisrelowllem2  37338  fvineqsneu  37393  fvineqsneq  37394  wl-cbvalnaed  37512  wl-2sb6d  37538  wl-sbalnae  37542  wl-mo2tf  37551  wl-eutf  37553  wl-ax11-lem3  37567  phpreu  37590  poimirlem26  37632  poimirlem27  37633  heicant  37641  mbfposadd  37653  ftc1anclem5  37683  indexdom  37720  filbcmb  37726  sdclem2  37728  sdclem1  37729  fdc1  37732  riotasv2d  38938  riotasv2s  38939  nfded2  38949  glbconxN  39360  pmapglb2xN  39754  cdlemefs32sn1aw  40396  mzpsubmpt  42730  mzpexpmpt  42732  eq0rabdioph  42763  eqrabdioph  42764  setindtr  43012  unielss  43206  nadd1suc  43381  ss2iundf  43648  scottabf  44235  mnuprdlem4  44270  ismnushort  44296  binomcxplemnotnn0  44351  iunconnlem2  44932  modelaxreplem3  44944  modelaxrep  44945  elunif  44953  rspcegf  44960  fnchoice  44966  refsumcn  44967  rfcnnnub  44973  uzwo4  44992  fiiuncl  45004  cbvmpo2  45036  cbvmpo1  45037  iinssiin  45068  disjf1  45125  disjrnmpt2  45130  disjf1o  45133  disjinfi  45134  choicefi  45142  axccdom  45164  dmrelrnrel  45168  axccd  45171  rnmptbddlem  45188  rnmptbd2lem  45192  infnsuprnmpt  45194  rnmptbdlem  45199  rnmptssbi  45205  upbdrech  45255  ssfiunibd  45259  supxrgere  45282  supxrgelem  45286  supxrge  45287  xralrple2  45303  infxr  45316  infxrunb2  45317  xrralrecnnle  45332  xrralrecnnge  45339  supxrunb3  45348  supxrleubrnmpt  45355  infleinf2  45363  unb2ltle  45364  rexabslelem  45367  suprleubrnmpt  45371  uzub  45380  supminfrnmpt  45394  supxrleubrnmptf  45400  infxrgelbrnmpt  45403  infrpgernmpt  45414  monoordxr  45432  monoord2xr  45434  caucvgbf  45439  cvgcaule  45441  iccshift  45470  iooshift  45474  iooiinicc  45494  iooiinioc  45508  fsummulc1f  45526  fsumf1of  45529  fsumreclf  45531  fsumlessf  45532  fmul01  45535  fmuldfeqlem1  45537  fmuldfeq  45538  fmul01lt1lem1  45539  fmul01lt1lem2  45540  fprodexp  45549  mccl  45553  fprodcnlem  45554  fprodcn  45555  climmulf  45559  climexp  45560  climsuse  45563  climrecf  45564  climinff  45566  climaddf  45570  mullimc  45571  islptre  45574  climf  45577  mullimcf  45578  rexlim2d  45580  idlimc  45581  limcperiod  45583  limcrecl  45584  islpcn  45594  limsupre  45596  limcleqr  45599  addlimc  45603  limclner  45606  climsubmpt  45615  climreclf  45619  climf2  45621  climeldmeqmpt  45623  clim2f2  45625  climfveqmpt  45626  fnlimfvre  45629  allbutfifvre  45630  climleltrp  45631  fnlimf  45633  fnlimabslt  45634  climfveqf  45635  climfveqmpt3  45637  climeldmeqf  45638  climeqf  45643  climeldmeqmpt3  45644  limsuppnfd  45657  limsupub  45659  climinf2lem  45661  climinf2  45662  limsuppnf  45666  limsupubuz  45668  climinf2mpt  45669  climinfmpt  45670  climinf3  45671  limsupmnflem  45675  limsupequz  45678  limsupre2  45680  limsupmnfuzlem  45681  limsupequzmptf  45686  limsupre3  45688  limsupre3uzlem  45690  limsupreuzmpt  45694  climisp  45701  lmbr3  45702  climrescn  45703  climxrrelem  45704  climxrre  45705  limsupub2  45767  liminflbuz2  45770  xlimmnfvlem2  45788  xlimmnfv  45789  xlimpnfvlem2  45792  xlimpnfv  45793  xlimmnfmpt  45798  xlimpnfmpt  45799  climxlim2lem  45800  cncficcgt0  45843  cncfioobd  45852  fprodsubrecnncnvlem  45862  fprodaddrecnncnvlem  45864  dvmptmulf  45892  dvnmul  45898  dvmptfprodlem  45899  dvmptfprod  45900  dvnprodlem1  45901  dvnprodlem2  45902  iblsplitf  45925  itgperiod  45936  stoweidlem3  45958  stoweidlem26  45981  stoweidlem27  45982  stoweidlem29  45984  stoweidlem31  45986  stoweidlem34  45989  stoweidlem35  45990  stoweidlem36  45991  stoweidlem39  45994  stoweidlem42  45997  stoweidlem43  45998  stoweidlem44  45999  stoweidlem46  46001  stoweidlem48  46003  stoweidlem49  46004  stoweidlem51  46006  stoweidlem52  46007  stoweidlem53  46008  stoweidlem54  46009  stoweidlem55  46010  stoweidlem56  46011  stoweidlem57  46012  stoweidlem58  46013  stoweidlem59  46014  stoweidlem60  46015  stoweidlem61  46016  stoweidlem62  46017  stoweid  46018  wallispilem3  46022  stirlinglem13  46041  stirling  46044  fourierdlem16  46078  fourierdlem21  46083  fourierdlem22  46084  fourierdlem31  46093  fourierdlem39  46101  fourierdlem48  46109  fourierdlem51  46112  fourierdlem68  46129  fourierdlem71  46132  fourierdlem73  46134  fourierdlem80  46141  fourierdlem81  46142  fourierdlem86  46147  fourierdlem87  46148  fourierdlem93  46154  fourierdlem94  46155  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  fourierdlem113  46174  elaa2  46189  etransclem32  46221  salexct  46289  sge0revalmpt  46333  sge0f1o  46337  sge0lefi  46353  sge0resplit  46361  sge0lempt  46365  sge0iunmptlemre  46370  sge0fodjrnlem  46371  sge0iunmpt  46373  sge0ltfirpmpt2  46381  sge0isum  46382  sge0xp  46384  sge0isummpt2  46387  sge0xadd  46390  sge0pnffsumgt  46397  sge0gtfsumgt  46398  sge0uzfsumgt  46399  sge0reuz  46402  sge0reuzb  46403  iundjiun  46415  meadjiun  46421  ismeannd  46422  voliunsge0lem  46427  meaiunincf  46438  meaiuninc3v  46439  meaiuninc3  46440  meaiininc  46442  caragenfiiuncl  46470  omeiunltfirp  46474  ovnsubaddlem2  46526  hoidmvval0  46542  hoidmvlelem1  46550  hoidmvlelem3  46552  hoidmvlelem5  46554  ovnlecvr2  46565  hspdifhsp  46571  hoiqssbllem2  46578  hoiqssbllem3  46579  hspmbllem2  46582  opnvonmbllem2  46588  hoimbl2  46620  vonhoire  46627  iinhoiicc  46629  iunhoiioolem  46630  iunhoiioo  46631  vonioo  46637  vonicc  46640  vonn0ioo2  46645  vonn0icc2  46647  salpreimagelt  46662  salpreimalegt  46664  pimincfltioc  46671  pimdecfgtioo  46672  pimincfltioo  46673  preimageiingt  46675  preimaleiinlt  46676  salpreimagtge  46680  salpreimaltle  46681  salpreimalelt  46684  salpreimagtlt  46685  incsmflem  46696  issmflelem  46699  issmfle  46700  smfconst  46704  issmfgtlem  46710  issmfgt  46711  smfaddlem2  46719  smfadd  46720  decsmflem  46721  decsmf  46722  issmfgelem  46724  issmfge  46725  smflimlem2  46727  smflim  46732  smfresal  46743  smfrec  46744  smfmullem4  46749  smfmul  46750  smfpimcc  46763  smflimmpt  46765  smfsuplem1  46766  smfsupmpt  46770  smfsupxr  46771  smfinflem  46772  smfinfmpt  46774  smflimsuplem5  46779  smflimsuplem7  46781  smflimsuplem8  46782  smflimsupmpt  46784  smfliminflem  46785  smfliminfmpt  46787  smfpimne2  46795  fsupdm  46797  smfsupdmmbllem  46799  finfdm  46801  smfinfdmmbllem  46803  or2expropbilem2  46982  or2expropbi  46983  cfsetsnfsetf  47007  2reu8i  47062  nfdfat  47076  iccelpart  47357  ichnfim  47388  ich2exprop  47395  ichreuopeq  47397  sprsymrelfo  47421  reupr  47446  reuopreuprim  47450  2zrngmmgm  48095  opeliun2xp  48177  cbvmpox2  48180  ovmpordxf  48183  1arymaptfo  48492  2arymaptfo  48503  setrec1  48921  pgindnf  48946  aacllem  49031