Theorem ancoms 469

Description: Inference commuting conjunction in antecedent. (Contributed by NM, 21-Apr-1994.)

Hypothesis

Ref	Expression
ancoms.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ancoms	⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Proof of Theorem ancoms

Step	Hyp	Ref	Expression
1		ancoms.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	expcom 451	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 445	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 384

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

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  adantl  482  syl2anr  495  anim12ci  591  sylan9bbr  737  anabss4  856  anabsi7  860  anabsi8  861  im2anan9r  881  bi2anan9r  918  syl3anr2  1379  mp3anr1  1421  mp3anr2  1422  mp3anr3  1423  stoic1b  1698  dvelimf  2334  2eu3  2555  eqeqan12rd  2640  sylan9eqr  2678  r19.29vva  3081  morex  3390  sbcrext  3511  sbcrextOLD  3512  sylan9ssr  3617  pssdifcom1  4054  pssdifcom2  4055  riinn0  4595  breqan12rd  4670  propeqop  4970  soinxp  5183  frinxp  5184  seinxp  5185  brelrng  5355  dminss  5547  imainss  5548  sossfld  5580  setlikespec  5701  ordelssne  5750  ordtri3or  5755  ordtri2  5758  ordtri4  5761  ordtr3OLD  5770  ordtri2or  5822  funsng  5937  f1co  6110  f1ocnv  6149  f1oprswap  6180  funimass4  6247  dffv2  6271  fndmdifcom  6322  fsn2  6403  fvtp2  6461  fvtp3  6462  fvtp2g  6464  fvtp3g  6465  soisoi  6578  riotaeqimp  6634  oveqan12rd  6670  brrpssg  6939  sorpsscmpl  6948  dfwe2  6981  ordsucelsuc  7022  ordunisuc2  7044  tfindsg  7060  tfindsg2  7061  dfom2  7067  funcnvuni  7119  fun11iun  7126  cofunex2g  7131  curry2  7272  soxp  7290  mpt2xopoveqd  7347  tposoprab  7388  wfr3g  7413  wfrlem5  7419  wfrlem10  7424  smores3  7450  smores2  7451  smoel  7457  dfrecs3  7469  tfr3  7495  tz7.48-2  7537  tz7.49  7540  oaordi  7626  oaword  7629  oaord1  7631  oaword2  7633  oa00  7639  oalimcl  7640  oaass  7641  oarec  7642  oacomf1o  7645  omord2  7647  omcan  7649  omword  7650  omword1  7653  omword2  7654  odi  7659  omass  7660  oneo  7661  oen0  7666  oecan  7669  oelim2  7675  nnarcl  7696  nnaordi  7698  nnaordr  7700  nnawordi  7701  nnmsucr  7705  nnmcom  7706  nnaword  7707  nnmordi  7711  nnaordex  7718  oaabslem  7723  omabslem  7726  nnneo  7731  omsmo  7734  ersym  7754  elecg  7785  riiner  7820  ecopovsym  7849  ecovcom  7854  mapvalg  7867  pmvalg  7868  elpmg  7873  elmapssres  7882  pmss12g  7884  ixpconstg  7917  ener  8002  enerOLD  8003  domtr  8009  f1imaeng  8016  fundmen  8030  xpcomco  8050  xpsnen2g  8053  xpdom2  8055  xpdom1g  8057  omxpen  8062  omf1o  8063  enen2  8101  domen2  8103  sdomen2  8105  domtriord  8106  sdomel  8107  onsdominel  8109  infensuc  8138  onomeneq  8150  nndomo  8154  pssnn  8178  unbnn  8216  infcntss  8234  fiint  8237  mapfi  8262  fiin  8328  fiss  8330  infempty  8412  oiiso  8442  unwdomg  8489  suc11reg  8516  inf3lem5  8529  infeq5  8534  cantnfp1lem3  8577  r1tr  8639  r1val1  8649  rankr1ai  8661  rankonidlem  8691  onssr1  8694  tskwe  8776  carddom2  8803  carden2  8813  domtri2  8815  cardval2  8817  fidomtri  8819  fidomtri2  8820  harval2  8823  dif1card  8833  infxpenlem  8836  ac5num  8859  alephord3  8901  alephdom  8904  aleph11  8907  alephdom2  8910  cardaleph  8912  dfac3  8944  dfac5  8951  cdacomen  9003  onacda  9019  pwsdompw  9026  ackbij1lem11  9052  ackbij2  9065  cfeq0  9078  cfsuc  9079  cff1  9080  cflim2  9085  cfsmolem  9092  coftr  9095  sornom  9099  infpssrlem4  9128  ssfin4  9132  ssfin2  9142  ssfin3ds  9152  fin23lem31  9165  isf32lem9  9183  hsmexlem5  9252  axdc3lem  9272  axdc3lem2  9273  axdc3lem4  9275  zorn2lem6  9323  brdom3  9350  brdom7disj  9353  brdom6disj  9354  alephval2  9394  alephreg  9404  wuncss  9567  gruen  9634  addcompi  9716  mulcompi  9718  ltapi  9725  ltmpi  9726  nqereu  9751  addcompq  9772  addcomnq  9773  mulcompq  9774  mulcomnq  9775  ltsonq  9791  ltanq  9793  ltmnq  9794  genpnnp  9827  addcompr  9843  mulcompr  9845  ltsopr  9854  ltexprlem2  9859  prlem936  9869  suplem2pr  9875  map2psrpr  9931  axpre-ltadd  9988  xrltnle  10105  axlttri  10109  axsup  10113  ltnle  10117  letri3  10123  leloe  10124  eqlelt  10125  letric  10137  mul31  10204  subcl  10280  pncan2  10288  pncan3  10289  npcan  10290  addsubeq4  10296  npncan3  10319  negsubdi2  10340  muladd  10462  subdi  10463  mulneg2  10467  mulsub  10473  ltleadd  10511  ltsubpos  10520  posdif  10521  addge01  10538  lesub0  10545  wloglei  10560  prodgt02  10869  prodge02  10871  mulsuble0b  10895  ltdivmul  10898  ledivmul  10899  lt2mul2div  10901  lerec  10906  lt2msq  10908  ltdiv23  10914  lediv23  10915  lediv2a  10917  le2msq  10923  msq11  10924  fimaxre  10968  lbreu  10973  infm3  10982  dfinfre  11004  creur  11014  creui  11015  cju  11016  nnmulcl  11043  nndivtr  11062  avgle1  11272  avgle2  11273  avgle  11274  nn0nnaddcl  11324  ltsubnn0  11344  zrevaddcl  11422  znnsub  11423  znn0sub  11424  zextlt  11451  gtndiv  11454  prime  11458  uztrn2  11705  uztric  11709  uz11  11710  nn0pzuz  11745  uzwo  11751  zmax  11785  zbtwnre  11786  rebtwnz  11787  qrevaddcl  11810  rpnnen1lem2  11814  rpnnen1lem1  11815  rpnnen1lem3  11816  rpnnen1lem5  11818  rpnnen1lem1OLD  11821  rpnnen1lem3OLD  11822  rpnnen1lem5OLD  11824  difrp  11868  xrltnsym  11970  xrlttri  11972  xrleloe  11977  xrletri  11984  xrletri3  11985  xrmaxeq  12010  xrmineq  12011  xrmaxlt  12012  xrmaxle  12014  lemaxle  12026  z2ge  12029  qbtwnre  12030  qextlt  12034  qextle  12035  xleneg  12049  xaddcom  12071  xmulcom  12096  xmulneg2  12100  xmulgt0  12113  xrsupsslem  12137  xrinfmsslem  12138  supxrunb1  12149  supxrunb2  12150  ixxssixx  12189  ixxin  12192  ioon0  12201  iccid  12220  iooshf  12252  iccsupr  12266  iooneg  12292  iccneg  12293  iccsplit  12305  fzen  12358  fzadd2  12376  fzass4  12379  fzrev  12403  fznn  12408  elfzp1b  12417  elfzm1b  12418  fz0fzdiffz0  12448  difelfznle  12453  fzon  12489  fzo0n  12490  fzonmapblen  12513  elfzoext  12524  eluzgtdifelfzo  12529  ubmelm1fzo  12564  elfzom1elp1fzo1  12568  subfzo0  12590  fllt  12607  flflp1  12608  flbi  12617  flbi2  12618  flzadd  12627  ltdifltdiv  12635  dfceil2  12640  modcyc2  12706  modifeq2int  12732  modaddmodup  12733  modaddmodlo  12734  modfzo0difsn  12742  modsumfzodifsn  12743  om2uzlt2i  12750  om2uzf1oi  12752  fseqsupubi  12777  fsuppmapnn0fiub0  12793  expcllem  12871  mulbinom2  12984  faclbnd5  13085  hashbnd  13123  hasheni  13136  hasheqf1oi  13140  hasheqf1oiOLD  13141  hashdom  13168  hashss  13197  hashfacen  13238  ccatsymb  13366  ccatass  13371  ccatalpha  13375  wrd2ind  13477  swrdccatin12lem2b  13486  swrdccatin2  13487  swrdccatin12lem2  13489  swrdccatin12  13491  swrdccat3blem  13495  swrdccatid  13497  repswsymball  13526  repswsymballbi  13527  cshwsublen  13542  cshwn  13543  cshwlen  13545  cshwidxmod  13549  cshf1  13556  repswcshw  13558  cshweqdif2  13565  cshweqrep  13567  cshwcsh2id  13574  ccatco  13581  swrdco  13583  lswco  13584  s3iunsndisj  13707  relexprelg  13778  relexpnndm  13781  relexpaddnn  13791  shftlem  13808  shftuz  13809  shftfval  13810  shftval4  13817  shftval5  13818  2shfti  13820  seqshft  13825  mulre  13861  sqrtlt  14002  abs3dif  14071  abs2difabs  14074  uzin2  14084  rexanre  14086  caubnd  14098  climshftlem  14305  rlimcn2  14321  fsumcnv  14504  modfsummods  14525  geo2lim  14606  ntrivcvgfvn0  14631  prodmo  14666  zprod  14667  prodss  14677  fprodcnv  14713  bpolysum  14784  bpoly4  14790  efle  14848  reef11  14849  demoivre  14930  demoivreALT  14931  znnenlem  14940  sqrt2irr  14979  nndivides  14990  0dvds  15002  muldvds1  15006  muldvds2  15007  dvdscmulr  15010  dvdssubr  15027  dvdsadd2b  15028  odd2np1  15065  mulsucdiv2z  15077  ltoddhalfle  15085  divalglem9  15124  ndvdssub  15133  gcdcllem1  15221  gcdcom  15235  neggcd  15244  gcdabs2  15252  modgcd  15253  lcmcom  15306  neglcm  15317  lcmgcdeq  15325  coprmdvds  15366  coprmdvdsOLD  15367  qredeq  15371  divgcdcoprmex  15380  dvdsprm  15415  cncongrprm  15437  odzdvds  15500  powm2modprm  15508  modprmn0modprm0  15512  coprimeprodsq  15513  pythagtriplem1  15521  pythagtriplem4  15524  pc2dvds  15583  pc11  15584  pcz  15585  pcprod  15599  prmunb  15618  1arithlem3  15629  1arith  15631  cshwshashlem2  15803  cshwshashlem3  15804  ressabs  15939  acsfn2  16324  issect  16413  funcestrcsetclem9  16788  funcsetcestrclem5  16799  funcsetcestrclem9  16803  pospo  16973  latjcom  17059  latmcom  17075  clatglbss  17127  pospropd  17134  pslem  17206  tsrss  17223  issubmnd  17318  submcl  17353  resmhm2b  17361  frmdmnd  17396  frmd0  17397  grpinvsub  17497  dfgrp3lem  17513  gimcnv  17709  gimco  17710  gictr  17717  cntz2ss  17765  cntzrec  17766  symg2bas  17818  symgextf1  17841  symgfixelsi  17855  pmtrfinv  17881  pmtrdifwrdel2  17906  dfod2  17981  lsmcom2  18070  efgred  18161  qusabl  18268  cygabl  18292  gsummptnn0fz  18382  eldprd  18403  srgmulgass  18531  dfrhm2  18717  isrim0  18723  rmodislmodlem  18930  rmodislmod  18931  lmimcnv  19067  mplcoe5lem  19467  psrbagfsupp  19509  cnfldexp  19779  cnsrng  19780  xrsdsreval  19791  dvdsrzring  19831  znf1o  19900  ocvocv  20015  ocvin  20018  frlmip  20117  islindf  20151  lindff  20154  lindfrn  20160  f1lindf  20161  mamudir  20210  matsca2  20226  matbas2  20227  matlmod  20235  matinvgcell  20241  mat1bas  20255  dmatmul  20303  dmatsgrp  20305  dmatsrng  20307  dmatcrng  20308  scmatsgrp1  20328  scmatsrng1  20329  madulid  20451  gsummatr01lem3  20463  gsummatr01  20465  cpmatacl  20521  0mat2pmat  20541  idmatidpmat  20542  m2cpminv0  20566  pmatcollpw3fi1lem1  20591  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  eltg  20761  eltg2  20762  tgss  20772  tgss2  20791  basgen2  20793  bastop1  20797  cldmre  20882  toponmre  20897  opnneiss  20922  restcldr  20978  restfpw  20983  restcls  20985  restntr  20986  ordtbaslem  20992  ordtrest2lem  21007  leordtvallem2  21015  leordtval  21017  cnrest  21089  t0sep  21128  cmpcov  21192  cmpsublem  21202  cmpsub  21203  bwth  21213  2ndcomap  21261  locfincmp  21329  ptval  21373  xkoval  21390  txss12  21408  ptrescn  21442  xkopt  21458  hmeofval  21561  txswaphmeolem  21607  txswaphmeo  21608  trfbas2  21647  trfbas  21648  uzrest  21701  numufl  21719  ssufl  21722  flimclsi  21782  hauspwpwf1  21791  ghmcnp  21918  blpnfctr  22241  metequiv  22314  metcnp3  22345  elbl4  22368  restmetu  22375  tngngp  22458  qtopbaslem  22562  bl2ioo  22595  ioo2bl  22596  ioo2blex  22597  xrsxmet  22612  divccn  22676  divccncf  22709  isclmi0  22898  iscvsi  22929  causs  23096  lmclim  23101  bcthlem1  23121  ovolfsf  23240  ioombl  23333  iccvolcl  23335  ioovolcl  23338  ioorcl  23345  volcn  23374  itg2itg1  23503  dvexp  23716  dvmptfsum  23738  dvexp3  23741  dvef  23743  dvlip  23756  c1lip1  23760  ftc1a  23800  tdeglem1  23818  tdeglem3  23819  tdeglem4  23820  coe1termlem  24014  plyremlem  24059  ptolemy  24248  cos11  24279  logeftb  24330  logleb  24349  logdivlt  24367  logdivle  24368  angval  24531  isppw2  24841  issqf  24862  vmasum  24941  lgsprme0  25064  gausslemma2dlem1a  25090  lgsquadlem3  25107  2lgsoddprmlem2  25134  ostth  25328  brbtwn2  25785  colinearalglem4  25789  ax5seglem1  25808  ax5seglem2  25809  axcontlem2  25845  axcontlem12  25855  upgrpredgv  26034  uhgr2edg  26100  issubgr  26163  subgrprop  26165  subuhgr  26178  subupgr  26179  subumgr  26180  subusgr  26181  nb3grprlem2  26283  cplgr3v  26331  wlk1walk  26535  upgrwlkvtxedg  26541  pthdivtx  26625  usgr2trlncl  26656  crctcshwlkn0lem3  26704  crctcshwlkn0lem6  26707  crctcshwlkn0lem7  26708  crctcshwlkn0  26713  wlkiswwlks2  26761  wwlksnextbi  26789  wwlksnfi  26801  wwlksnextprop  26807  clwwlksfo  26918  erclwwlkssym  26935  erclwwlksnsym  26947  is0wlk  26978  is0trl  26984  3pthdlem1  27024  frgr3v  27139  frgrncvvdeqlem3  27165  frgrregorufr  27189  numclwwlkovf2exlem2  27212  numclwwlkovfel2  27216  numclwwlk1  27231  numclwlk2lem2f  27236  numclwlk2lem2f1o  27238  frgrregord013  27253  vcz  27430  isvcOLD  27434  isnv  27467  isnvi  27468  nmooge0  27622  nmblolbii  27654  blocnilem  27659  ipblnfi  27711  hvpncan2  27897  hvaddsub4  27935  hire  27951  abshicom  27958  hial2eq2  27964  orthcom  27965  hhssabloi  28119  ocsh  28142  shscli  28176  shscom  28178  shsel2  28181  spanss  28207  shjcom  28217  shmodsi  28248  chpsscon3  28362  spansni  28416  spansnmul  28423  spansncol  28427  spanunsni  28438  cmcm2  28475  cm2j  28479  spansncvi  28511  5oalem2  28514  3oalem2  28522  honegsubdi2  28670  adjsym  28692  cnvadj  28751  brafn  28806  kbpj  28815  riesz3i  28921  cnlnadjlem2  28927  cnlnadjlem9  28934  nmopcoi  28954  cnvbraval  28969  leop  28982  leop3  28984  leopmul2i  28994  leoptri  28995  hstrlem3a  29119  cvcon3  29143  cvnsym  29149  mdbr2  29155  dmdmd  29159  dmdbr2  29162  dmdbr3  29164  dmdbr4  29165  dmdbr5  29167  mdsl0  29169  ssmd2  29171  mdslmd1lem1  29184  mdslmd1lem2  29185  mdslmd3i  29191  mdslmd4i  29192  atcveq0  29207  superpos  29213  atnemeq0  29236  atssma  29237  atexch  29240  atomli  29241  atcvatlem  29244  atcvati  29245  chirredlem1  29249  chirredlem3  29251  chirredi  29253  atcvat3i  29255  atdmd  29257  mdsymlem1  29262  mdsymlem3  29264  mdsymlem4  29265  mdsymlem5  29266  mdsymlem8  29269  dmdsym  29272  atdmd2  29273  sumdmdlem  29277  cdjreui  29291  cdj3lem2b  29296  cdj3i  29300  r19.29ffa  29320  imadifxp  29414  abfmpel  29455  xaddeq0  29518  xrofsup  29533  xeqlelt  29538  xdivpnfrp  29641  xrsinvgval  29677  xrsmulgzz  29678  pcmplfin  29927  cnvordtrestixx  29959  ordtrest2NEWlem  29968  indval  30075  esumpfinvallem  30136  sigagenss  30212  ddemeas  30299  brae  30304  dya2iocival  30335  dya2iocnei  30344  dya2iocuni  30345  omsf  30358  oddpwdc  30416  bnj934  31005  derangenlem  31153  subfacval2  31169  kur14  31198  lediv2aALT  31571  dford5  31608  faclim2  31634  funpsstri  31663  dftrpred3g  31733  soseq  31751  wsuclem  31773  wsuclemOLD  31774  frrlem5  31784  elno  31799  nosepon  31818  noextenddif  31821  sltsolem1  31826  nosepne  31831  nolt02o  31845  sltnle  31878  sleloe  31879  sletri3  31880  hfelhf  32288  elicc3  32311  nn0prpwlem  32317  nn0prpw  32318  isfne  32334  onsuct0  32440  nndivsub  32456  bj-ssbequ2  32643  bj-restsnss  33036  bj-restsnss2  33037  bj-restuni2  33051  topdifinffinlem  33195  iooelexlt  33210  relowlssretop  33211  rdgeqoa  33218  wl-sbcom2d-lem1  33342  wl-sbcom2d  33344  wl-ax11-lem6  33367  curf  33387  finixpnum  33394  ltflcei  33397  leceifl  33398  cos2h  33400  matunitlindflem1  33405  matunitlindflem2  33406  matunitlindf  33407  ptrecube  33409  poimirlem6  33415  poimirlem7  33416  poimirlem10  33419  poimirlem11  33420  poimirlem27  33436  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  cnambfre  33458  itg2addnclem2  33462  itg2addnc  33464  itg2gt0cn  33465  ftc1anclem1  33485  ftc1anclem4  33488  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anc  33493  unirep  33507  opelopab3  33511  fvopabf4g  33515  indexa  33528  filbcmb  33535  incsequz2  33545  metf1o  33551  sstotbnd3  33575  isbnd2  33582  bndss  33585  ismtycnv  33601  iccbnd  33639  exidreslem  33676  exidresid  33678  ghomco  33690  isdivrngo  33749  isdrngo2  33757  rngoisocnv  33780  riscer  33787  crngohomfo  33805  unichnidl  33830  maxidlmax  33842  igenmin  33863  exmid2  33901  orel  33904  prtlem16  34154  paddss1  35103  paddss2  35104  paddss12  35105  pclfinN  35186  erngmul-rN  36102  mapdordlem2  36926  ismrc  37264  nacsfg  37268  isnacs3  37273  incssnn0  37274  mzpclall  37290  lerabdioph  37369  ltrabdioph  37372  eldioph4b  37375  jm2.17b  37528  congrep  37540  lnr2i  37686  rp-fakenanass  37860  brnonrel  37895  enrelmap  38291  enrelmapr  38292  rcompleq  38318  isotone1  38346  isotone2  38347  radcnvrat  38513  expgrowth  38534  bcc0  38539  binomcxplemnn0  38548  2sbc6g  38616  2sbc5g  38617  ordpss  38655  addrcom  38679  3impcombi  39044  sspwimp  39154  sspwimpVD  39155  ax6e2ndeqALT  39167  iunconnlem2  39171  sineq0ALT  39173  nsstr  39273  iunmapsn  39409  ssfiunibd  39523  fmul01  39812  lptre2pt  39872  stoweidlem34  40251  dirkeritg  40319  fourierdlem73  40396  smfsuplem1  41017  smfinflem  41023  sigarac  41041  2reu3  41188  afv0nbfvbi  41231  dmfcoafv  41255  cnambpcma  41309  ltnltne  41313  fzoopth  41337  elmod2  41340  pfxccatin12lem1  41423  pfxccatin12lem2  41424  pfxccatin12  41425  fmtnofac2lem  41480  prmdvdsfmtnof1lem2  41497  proththd  41531  opoeALTV  41594  opeoALTV  41595  epoo  41612  evenprm2  41623  gbegt5  41649  sbgoldbaltlem2  41668  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  bgoldbtbndlem4  41696  bgoldbtbnd  41697  sprsymrelfolem2  41743  sprsymrelf1  41746  uspgrsprfo  41756  submgmcl  41794  resmgmhm2b  41800  isassintop  41846  rnghmval  41891  isrngisom  41896  c0snghm  41916  zrrnghm  41917  2zrngamgm  41939  rnghmsubcsetclem2  41976  rhmsubcsetclem2  42022  rhmsubcrngclem1  42027  rhmsubcrngclem2  42028  funcringcsetcALTV2lem9  42044  funcringcsetclem9ALTV  42067  rhmsubclem4  42089  rhmsubcALTVlem4  42107  cbvmpt2x2  42114  nn0sumltlt  42128  gsumlsscl  42164  ply1mulgsumlem1  42174  lincvalpr  42207  lincdifsn  42213  linc1  42214  lincellss  42215  islinindfiss  42239  islindeps  42242  lincresunit2  42267  islininds2  42273  lmod1zr  42282  ltsubadd2b  42306  zgtp1leeq  42311  logblt1b  42358  blengt1fldiv2p1  42387  nn0sumshdiglemB  42414  aacllem  42547