Theorem nfan 1990

Description: If 𝑥 is not free in 𝜑 and 𝜓, 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 1988	. 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ∧ 𝜓))
6	5	mptru 1645	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Syntax hints:   ∧ wa 384  ⊤wtru 1638  Ⅎwnf 1863

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

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864

This theorem is referenced by:  nfnan  1992  nf3an  1993  hban  2304  nfeqf  2469  nfald2  2493  nfsb4t  2548  2ax6elem  2609  eupicka  2701  mopick2  2704  2mo  2715  axbnd  2783  clelab  2932  nfabd2  2968  2ralbida  3175  r19.29an  3265  ralcom2  3292  reean  3294  cbvreu  3358  cbvrab  3388  ceqsex2  3438  vtocl2gaf  3466  rspce  3497  eqvincf  3525  elrabf  3555  elrab3t  3558  rexab2  3569  morex  3588  reu2  3592  reu2eqd  3601  sbc2iegf  3700  reu8nf  3711  rmo2  3721  rmo3  3723  csbiebt  3748  csbie2t  3757  cbvreucsf  3762  cbvrabcsf  3763  rabsnifsb  4448  nfop  4611  nfopd  4612  eluniab  4641  nfopab  4912  cbvopab  4915  cbvopab1  4917  cbvopab2  4918  cbvopab1s  4919  mpteq12f  4925  nfmpt  4940  cbvmptf  4942  cbvmpt  4943  axrep3  4968  axrep4  4969  axrep5  4970  reusv2lem3  5069  nfpo  5237  nfso  5238  nffr  5285  nfwe  5287  nfxp  5343  opeliunxp  5370  nfco  5489  elrnmpt1  5575  nfimad  5685  iota2  6090  nffun  6124  imadif  6184  nffn  6198  nff  6252  nff1  6314  nffo  6330  nff1o  6351  nffvd  6420  fv3  6426  f1ossf1o  6618  fmptco  6619  fsnex  6762  nfiso  6796  nfriotad  6843  cbvriota  6845  riota2df  6855  riota5f  6860  oprabv  6933  nfoprab  6937  mpt2eq123  6944  nfmpt2  6954  cbvoprab1  6957  cbvoprab2  6958  cbvoprab12  6959  cbvoprab3  6961  cbvmpt2x  6963  ovmpt2dxf  7016  elovmpt2rab  7110  elovmpt2rab1  7111  onminex  7237  peano5  7319  fun11iun  7356  opabex3d  7375  opabex3  7376  dfoprab4f  7458  fmpt2x  7469  opeliunxp2f  7571  nfwrecs  7644  wfrlem4  7653  wfrlem4OLD  7654  tfr3  7731  tz7.49  7776  erovlem  8079  nfixp  8164  nfixp1  8165  xpf1o  8361  nneneq  8382  ac6sfi  8443  nfoi  8658  wdom2d  8724  infpssrlem4  9413  hsmexlem2  9534  hsmexlem4  9536  domtriomlem  9549  axdc3lem2  9558  axdc4lem  9562  zorn2lem4  9606  zorn2lem5  9607  konigthlem  9675  axextnd  9698  axrepndlem2  9700  axrepnd  9701  axunnd  9703  axpowndlem2  9705  axpowndlem4  9707  axpownd  9708  axregndlem2  9710  axregnd  9711  axinfndlem1  9712  axinfnd  9713  zfcndrep  9721  zfcndinf  9725  dedekind  10485  dedekindle  10486  fsuppmapnn0fiublem  13013  fsuppmapnn0fiub  13014  fsuppmapnn0fiubex  13015  reuccats1  13704  nfsum1  14643  nfsum  14644  fsumsplitf  14695  fsum2dlem  14724  fsum00  14752  nfcprod1  14861  nfcprod  14862  fprod2dlem  14931  fprodsplitf  14939  fprodsplit1f  14941  fprodle  14947  lcmfunsnlem1  15569  lcmfunsnlem2lem1  15570  lcmfunsnlem2  15572  mreexexd  16513  acsmapd  17383  gsum2d2lem  18573  dprd2d2  18645  gsummoncoe1  19882  gsummatr01lem4  20676  cpmatmcllem  20736  cayleyhamilton1  20910  neiptopnei  21150  neiptopreu  21151  neitr  21198  iunconnlem  21444  iunconn  21445  ptcnplem  21638  ptcnp  21639  xkocnv  21831  isfildlem  21874  utopsnneiplem  22264  isucn2  22296  cfilucfil  22577  restmetu  22588  ovolfiniun  23482  ovoliunlem3  23485  ovoliunnul  23488  volfiniun  23528  itg2splitlem  23729  itg2split  23730  isibl2  23747  nfitg  23755  cbvitg  23756  limciun  23872  istrkg2ld  25573  chirred  29582  spc2ed  29640  mo5f  29652  rmo3f  29661  rmo4fOLD  29662  foresf1o  29668  cbvdisjf  29710  disjabrex  29720  disjabrexf  29721  funimass4f  29764  fmptcof2  29784  fcomptf  29785  acunirnmpt2  29787  acunirnmpt2f  29788  aciunf1lem  29789  funcnv4mpt  29797  cnvoprabOLD  29825  f1od2  29826  fpwrelmap  29835  xrofsup  29860  nn0min  29894  fprodex01  29898  fsumiunle  29902  2sqmo  29974  isarchiofld  30142  reff  30231  locfinreflem  30232  cmpcref  30242  ordtconnlem1  30295  prodindf  30410  esumcl  30417  gsumesum  30446  esumlub  30447  esumcst  30450  esumrnmpt2  30455  esumfzf  30456  esumfsup  30457  hasheuni  30472  esumcvg  30473  esumgect  30477  esumcvgre  30478  esum2dlem  30479  esum2d  30480  esumiun  30481  ldsysgenld  30548  sigapildsyslem  30549  sigapildsys  30550  ldgenpisyslem1  30551  measvunilem  30600  measvunilem0  30601  measvuni  30602  measinblem  30608  voliune  30617  volfiniune  30618  volmeas  30619  oms0  30684  omssubadd  30687  eulerpartlemgvv  30763  dstrvprob  30858  breprexplema  31033  bnj919  31160  bnj1146  31185  bnj1379  31224  bnj849  31318  bnj916  31326  bnj964  31336  bnj1014  31353  bnj1123  31377  bnj1228  31402  bnj1307  31414  bnj1321  31418  bnj1398  31425  bnj1408  31427  bnj1444  31434  bnj1445  31435  bnj1446  31436  bnj1449  31439  bnj1467  31445  bnj1463  31446  bnj1489  31447  bnj1491  31448  bnj1312  31449  bnj1525  31460  cvmcov  31568  iota5f  31928  axextdist  32025  axext4dist  32026  trpredmintr  32051  nfwlim  32088  nffrecs  32099  frrlem4  32104  finminlem  32633  bj-axrep3  33104  bj-axrep4  33105  bj-axrep5  33106  bj-dvelimdv  33146  isbasisrelowllem1  33519  isbasisrelowllem2  33520  wl-cbvalnaed  33633  wl-2sb6d  33655  wl-sbalnae  33659  wl-mo2tf  33667  wl-eutf  33669  wl-ax11-lem3  33678  phpreu  33706  poimirlem26  33748  poimirlem27  33749  heicant  33757  mbfposadd  33769  ftc1anclem5  33801  indexdom  33841  filbcmb  33847  sdclem2  33849  sdclem1  33850  fdc1  33853  riotasv2d  34736  riotasv2s  34737  nfded2  34748  glbconxN  35158  pmapglb2xN  35552  cdlemefs32sn1aw  36195  mzpsubmpt  37808  mzpexpmpt  37810  eq0rabdioph  37842  eqrabdioph  37843  setindtr  38092  ss2iundf  38451  binomcxplemnotnn0  39055  iunconnlem2  39665  elunif  39669  rspcegf  39676  fnchoice  39682  refsumcn  39683  rfcnnnub  39689  uzwo4  39714  fiiuncl  39727  cbvmpt22  39770  cbvmpt21  39771  iinssiin  39803  ralimda  39817  disjf1  39858  wessf1ornlem  39860  disjrnmpt2  39864  disjf1o  39867  fompt  39868  disjinfi  39869  choicefi  39879  axccdom  39903  dmrelrnrel  39906  axccd  39913  funimassd  39915  rnmptbddlem  39939  rnmptbd2lem  39946  infnsuprnmpt  39948  rnmptbdlem  39953  rnmptssbi  39960  upbdrech  40000  ssfiunibd  40004  supxrgere  40029  supxrgelem  40033  supxrge  40034  xralrple2  40050  infxr  40063  infxrunb2  40064  xrralrecnnle  40082  xrralrecnnge  40092  supxrunb3  40102  supxrleubrnmpt  40111  infleinf2  40120  unb2ltle  40121  rexabslelem  40124  suprleubrnmpt  40128  uzub  40137  supminfrnmpt  40151  supxrleubrnmptf  40159  infxrgelbrnmpt  40162  infrpgernmpt  40174  monoordxr  40192  monoord2xr  40194  iccshift  40225  iooshift  40229  iooiinicc  40249  iooiinioc  40263  fsumclf  40281  fsummulc1f  40282  fsumsplit1  40284  fsumf1of  40286  fsumreclf  40288  fsumlessf  40289  fmul01  40292  fmuldfeqlem1  40294  fmuldfeq  40295  fmul01lt1lem1  40296  fmul01lt1lem2  40297  fprodexp  40306  mccl  40310  fprodcnlem  40311  fprodcn  40312  climmulf  40316  climexp  40317  climsuse  40320  climrecf  40321  climinff  40323  climaddf  40327  mullimc  40328  islptre  40331  climf  40334  mullimcf  40335  rexlim2d  40337  idlimc  40338  limcperiod  40340  limcrecl  40341  islpcn  40351  limsupre  40353  limcleqr  40356  addlimc  40360  limclner  40363  climsubmpt  40372  climreclf  40376  climf2  40378  climeldmeqmpt  40380  clim2f2  40382  climfveqmpt  40383  fnlimfvre  40386  allbutfifvre  40387  climleltrp  40388  fnlimf  40390  fnlimabslt  40391  climfveqf  40392  climfveqmpt3  40394  climeldmeqf  40395  climeqf  40400  climeldmeqmpt3  40401  limsuppnfd  40414  limsupub  40416  climinf2lem  40418  climinf2  40419  limsuppnf  40423  limsupubuz  40425  climinf2mpt  40426  climinfmpt  40427  climinf3  40428  limsupmnflem  40432  limsupequz  40435  limsupre2  40437  limsupmnfuzlem  40438  limsupequzmptf  40443  limsupre3  40445  limsupre3uzlem  40447  limsupreuzmpt  40451  climisp  40458  lmbr3  40459  climrescn  40460  climxrrelem  40461  climxrre  40462  xlimmnfvlem2  40539  xlimmnfv  40540  xlimpnfvlem2  40543  xlimpnfv  40544  xlimmnfmpt  40549  xlimpnfmpt  40550  climxlim2lem  40551  cncficcgt0  40581  cncfioobd  40590  fprodsubrecnncnvlem  40601  fprodaddrecnncnvlem  40603  dvmptmulf  40632  dvnmul  40638  dvmptfprodlem  40639  dvmptfprod  40640  dvnprodlem1  40641  dvnprodlem2  40642  iblsplitf  40665  itgperiod  40676  stoweidlem3  40699  stoweidlem26  40722  stoweidlem27  40723  stoweidlem29  40725  stoweidlem31  40727  stoweidlem34  40730  stoweidlem35  40731  stoweidlem36  40732  stoweidlem39  40735  stoweidlem42  40738  stoweidlem43  40739  stoweidlem44  40740  stoweidlem46  40742  stoweidlem48  40744  stoweidlem49  40745  stoweidlem51  40747  stoweidlem52  40748  stoweidlem53  40749  stoweidlem54  40750  stoweidlem55  40751  stoweidlem56  40752  stoweidlem57  40753  stoweidlem58  40754  stoweidlem59  40755  stoweidlem60  40756  stoweidlem61  40757  stoweidlem62  40758  stoweid  40759  wallispilem3  40763  stirlinglem13  40782  stirling  40785  fourierdlem16  40819  fourierdlem21  40824  fourierdlem22  40825  fourierdlem31  40834  fourierdlem39  40842  fourierdlem48  40850  fourierdlem51  40853  fourierdlem53  40855  fourierdlem68  40870  fourierdlem71  40873  fourierdlem73  40875  fourierdlem80  40882  fourierdlem81  40883  fourierdlem86  40888  fourierdlem87  40889  fourierdlem93  40895  fourierdlem94  40896  fourierdlem103  40905  fourierdlem104  40906  fourierdlem112  40914  fourierdlem113  40915  elaa2  40930  etransclem32  40962  salexct  41031  sge0revalmpt  41074  sge0f1o  41078  sge0lefi  41094  sge0resplit  41102  sge0lempt  41106  sge0iunmptlemre  41111  sge0fodjrnlem  41112  sge0iunmpt  41114  sge0ltfirpmpt2  41122  sge0isum  41123  sge0xp  41125  sge0isummpt2  41128  sge0xadd  41131  sge0pnffsumgt  41138  sge0gtfsumgt  41139  sge0uzfsumgt  41140  sge0reuz  41143  sge0reuzb  41144  iundjiun  41156  meadjiun  41162  ismeannd  41163  voliunsge0lem  41168  meaiunincf  41179  meaiuninc3v  41180  meaiuninc3  41181  meaiininc  41183  caragenfiiuncl  41211  omeiunltfirp  41215  ovnsubaddlem2  41267  hoidmvval0  41283  hoidmvlelem1  41291  hoidmvlelem3  41293  hoidmvlelem5  41295  ovnlecvr2  41306  hspdifhsp  41312  hoiqssbllem2  41319  hoiqssbllem3  41320  hspmbllem2  41323  opnvonmbllem2  41329  hoimbl2  41361  vonhoire  41368  iinhoiicc  41370  iunhoiioolem  41371  iunhoiioo  41372  vonioo  41378  vonicc  41381  vonn0ioo2  41386  vonn0icc2  41388  salpreimagelt  41400  salpreimalegt  41402  pimincfltioc  41408  pimdecfgtioo  41409  pimincfltioo  41410  preimageiingt  41412  preimaleiinlt  41413  salpreimagtge  41416  salpreimaltle  41417  salpreimalelt  41420  salpreimagtlt  41421  incsmflem  41432  issmflelem  41435  issmfle  41436  smfconst  41440  issmfgtlem  41446  issmfgt  41447  smfaddlem2  41454  smfadd  41455  decsmflem  41456  decsmf  41457  issmfgelem  41459  issmfge  41460  smflimlem2  41462  smflim  41467  smfresal  41477  smfrec  41478  smfmullem4  41483  smfmul  41484  smfpimcc  41496  smflimmpt  41498  smfsuplem1  41499  smfsupmpt  41503  smfsupxr  41504  smfinflem  41505  smfinfmpt  41507  smflimsuplem5  41512  smflimsuplem7  41514  smflimsuplem8  41515  smflimsupmpt  41517  smfliminflem  41518  smfliminfmpt  41520  nfdfat  41716  iccelpart  41944  sprsymrelfo  42315  2zrngmmgm  42514  opeliun2xp  42679  cbvmpt2x2  42682  ovmpt2rdxf  42685  setrec1  43006  aacllem  43118