MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancoms Structured version   Visualization version   GIF version

Theorem ancoms 468
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
StepHypRef Expression
1 ancoms.1 . . 3 ((𝜑𝜓) → 𝜒)
21expcom 450 . 2 (𝜓 → (𝜑𝜒))
32imp 444 1 ((𝜓𝜑) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 385
This theorem is referenced by:  adantl  481  syl2anr  494  anim12ci  590  sylan9bbr  737  anabss4  873  anabsi7  877  anabsi8  878  im2anan9r  899  bi2anan9r  936  syl3anr2  1419  mp3anr1  1461  mp3anr2  1462  mp3anr3  1463  stoic1b  1738  dvelimf  2365  2eu3  2584  eqeqan12rd  2669  sylan9eqr  2707  r19.29vva  3110  morex  3423  sbcrext  3544  sbcrextOLD  3545  sylan9ssr  3650  pssdifcom1  4087  pssdifcom2  4088  riinn0  4627  breqan12rd  4702  propeqop  4999  soinxp  5217  frinxp  5218  seinxp  5219  brelrng  5387  dminss  5582  imainss  5583  sossfld  5615  cnvsng  5652  setlikespec  5739  ordelssne  5788  ordtri3or  5793  ordtri2  5796  ordtri4  5799  ordtr3OLD  5808  ordtri2or  5860  funsng  5975  f1co  6148  f1ocnv  6187  f1oprswap  6218  funimass4  6286  dffv2  6310  fndmdifcom  6362  fsn2  6443  fvtp2  6502  fvtp3  6503  fvtp2g  6505  fvtp3g  6506  soisoi  6618  riotaeqimp  6674  oveqan12rd  6710  brrpssg  6981  sorpsscmpl  6990  dfwe2  7023  ordsucelsuc  7064  ordunisuc2  7086  tfindsg  7102  tfindsg2  7103  dfom2  7109  funcnvuni  7161  fun11iun  7168  cofunex2g  7173  curry2  7317  soxp  7335  mpt2xopoveqd  7392  tposoprab  7433  wfr3g  7458  wfrlem5  7464  wfrlem10  7469  smores3  7495  smores2  7496  smoel  7502  dfrecs3  7514  tfr3  7540  tz7.48-2  7582  tz7.49  7585  oaordi  7671  oaword  7674  oaord1  7676  oaword2  7678  oa00  7684  oalimcl  7685  oaass  7686  oarec  7687  oacomf1o  7690  omord2  7692  omcan  7694  omword  7695  omword1  7698  omword2  7699  odi  7704  omass  7705  oneo  7706  oen0  7711  oecan  7714  oelim2  7720  nnarcl  7741  nnaordi  7743  nnaordr  7745  nnawordi  7746  nnmsucr  7750  nnmcom  7751  nnaword  7752  nnmordi  7756  nnaordex  7763  oaabslem  7768  omabslem  7771  nnneo  7776  omsmo  7779  ersym  7799  elecg  7828  riiner  7863  ecopovsym  7892  ecovcom  7896  mapvalg  7909  pmvalg  7910  elpmg  7915  elmapssres  7924  pmss12g  7926  ixpconstg  7959  ener  8044  domtr  8050  f1imaeng  8057  fundmen  8071  xpcomco  8091  xpsnen2g  8094  xpdom2  8096  xpdom1g  8098  omxpen  8103  omf1o  8104  enen2  8142  domen2  8144  sdomen2  8146  domtriord  8147  sdomel  8148  onsdominel  8150  infensuc  8179  onomeneq  8191  nndomo  8195  pssnn  8219  unbnn  8257  infcntss  8275  fiint  8278  mapfi  8303  fiin  8369  fiss  8371  infempty  8453  oiiso  8483  unwdomg  8530  suc11reg  8554  inf3lem5  8567  infeq5  8572  cantnfp1lem3  8615  r1tr  8677  r1val1  8687  rankr1ai  8699  rankonidlem  8729  onssr1  8732  tskwe  8814  carddom2  8841  carden2  8851  domtri2  8853  cardval2  8855  fidomtri  8857  fidomtri2  8858  harval2  8861  dif1card  8871  infxpenlem  8874  ac5num  8897  alephord3  8939  alephdom  8942  aleph11  8945  alephdom2  8948  cardaleph  8950  dfac3  8982  dfac5  8989  cdacomen  9041  onacda  9057  pwsdompw  9064  ackbij1lem11  9090  ackbij2  9103  cfeq0  9116  cfsuc  9117  cff1  9118  cflim2  9123  cfsmolem  9130  coftr  9133  sornom  9137  infpssrlem4  9166  ssfin4  9170  ssfin2  9180  ssfin3ds  9190  fin23lem31  9203  isf32lem9  9221  hsmexlem5  9290  axdc3lem  9310  axdc3lem2  9311  axdc3lem4  9313  zorn2lem6  9361  brdom3  9388  brdom7disj  9391  brdom6disj  9392  alephval2  9432  alephreg  9442  wuncss  9605  gruen  9672  addcompi  9754  mulcompi  9756  ltapi  9763  ltmpi  9764  nqereu  9789  addcompq  9810  addcomnq  9811  mulcompq  9812  mulcomnq  9813  ltsonq  9829  ltanq  9831  ltmnq  9832  genpnnp  9865  addcompr  9881  mulcompr  9883  ltsopr  9892  ltexprlem2  9897  prlem936  9907  suplem2pr  9913  map2psrpr  9969  axpre-ltadd  10026  xrltnle  10143  axlttri  10147  axsup  10151  ltnle  10155  letri3  10161  leloe  10162  eqlelt  10163  letric  10175  mul31  10242  subcl  10318  pncan2  10326  pncan3  10327  npcan  10328  addsubeq4  10334  npncan3  10357  negsubdi2  10378  muladd  10500  subdi  10501  mulneg2  10505  mulsub  10511  ltleadd  10549  ltsubpos  10558  posdif  10559  addge01  10576  lesub0  10583  wloglei  10598  prodgt02  10907  prodge02  10909  mulsuble0b  10933  ltdivmul  10936  ledivmul  10937  lt2mul2div  10939  lerec  10944  lt2msq  10946  ltdiv23  10952  lediv23  10953  lediv2a  10955  le2msq  10961  msq11  10962  fimaxre  11006  lbreu  11011  infm3  11020  dfinfre  11042  creur  11052  creui  11053  cju  11054  nnmulcl  11081  nndivtr  11100  avgle1  11310  avgle2  11311  avgle  11312  nn0nnaddcl  11362  ltsubnn0  11382  zrevaddcl  11460  znnsub  11461  znn0sub  11462  zextlt  11489  gtndiv  11492  prime  11496  uztrn2  11743  uztric  11747  uz11  11748  nn0pzuz  11783  uzwo  11789  zmax  11823  zbtwnre  11824  rebtwnz  11825  qrevaddcl  11848  rpnnen1lem2  11852  rpnnen1lem1  11853  rpnnen1lem3  11854  rpnnen1lem5  11856  rpnnen1lem1OLD  11859  rpnnen1lem3OLD  11860  rpnnen1lem5OLD  11862  difrp  11906  xrltnsym  12008  xrlttri  12010  xrleloe  12015  xrletri  12022  xrletri3  12023  xrmaxeq  12048  xrmineq  12049  xrmaxlt  12050  xrmaxle  12052  lemaxle  12064  z2ge  12067  qbtwnre  12068  qextlt  12072  qextle  12073  xleneg  12087  xaddcom  12109  xmulcom  12134  xmulneg2  12138  xmulgt0  12151  xrsupsslem  12175  xrinfmsslem  12176  supxrunb1  12187  supxrunb2  12188  ixxssixx  12227  ixxin  12230  ioon0  12239  iccid  12258  iooshf  12290  iccsupr  12304  iooneg  12330  iccneg  12331  iccsplit  12343  fzen  12396  fzadd2  12414  fzass4  12417  fzrev  12441  fznn  12446  elfzp1b  12455  elfzm1b  12456  fz0fzdiffz0  12487  difelfznle  12492  fzon  12528  fzo0n  12529  fzonmapblen  12553  elfzoext  12564  eluzgtdifelfzo  12569  ubmelm1fzo  12604  elfzom1elp1fzo1  12608  subfzo0  12630  fllt  12647  flflp1  12648  flbi  12657  flbi2  12658  flzadd  12667  ltdifltdiv  12675  dfceil2  12680  modcyc2  12746  modifeq2int  12772  modaddmodup  12773  modaddmodlo  12774  modfzo0difsn  12782  modsumfzodifsn  12783  om2uzlt2i  12790  om2uzf1oi  12792  fseqsupubi  12817  fsuppmapnn0fiub0  12833  expcllem  12911  mulbinom2  13024  faclbnd5  13125  hashbnd  13163  hasheni  13176  hasheqf1oi  13180  hashdom  13206  hashss  13235  hashfacen  13276  ccatsymb  13400  ccatass  13406  ccatalpha  13411  wrd2ind  13523  swrdccatin12lem2b  13532  swrdccatin2  13533  swrdccatin12lem2  13535  swrdccatin12  13537  swrdccat3blem  13541  swrdccatid  13543  repswsymball  13572  repswsymballbi  13573  cshwsublen  13588  cshwn  13589  cshwlen  13591  cshwidxmod  13595  cshf1  13602  repswcshw  13604  cshweqdif2  13611  cshweqrep  13613  cshwcsh2id  13620  ccatco  13627  swrdco  13629  lswco  13630  s3iunsndisj  13753  relexprelg  13822  relexpnndm  13825  relexpaddnn  13835  shftlem  13852  shftuz  13853  shftfval  13854  shftval4  13861  shftval5  13862  2shfti  13864  seqshft  13869  mulre  13905  sqrtlt  14046  abs3dif  14115  abs2difabs  14118  uzin2  14128  rexanre  14130  caubnd  14142  climshftlem  14349  rlimcn2  14365  fsumcnv  14548  modfsummods  14569  geo2lim  14650  ntrivcvgfvn0  14675  prodmo  14710  zprod  14711  prodss  14721  fprodcnv  14757  bpolysum  14828  bpoly4  14834  efle  14892  reef11  14893  demoivre  14974  demoivreALT  14975  znnenlem  14984  sqrt2irr  15023  nndivides  15037  0dvds  15049  muldvds1  15053  muldvds2  15054  dvdscmulr  15057  dvdssubr  15074  dvdsadd2b  15075  odd2np1  15112  mulsucdiv2z  15124  ltoddhalfle  15132  divalglem9  15171  ndvdssub  15180  gcdcllem1  15268  gcdcom  15282  neggcd  15291  gcdabs2  15299  modgcd  15300  lcmcom  15353  neglcm  15364  lcmgcdeq  15372  coprmdvds  15413  coprmdvdsOLD  15414  qredeq  15418  divgcdcoprmex  15427  dvdsprm  15462  cncongrprm  15484  odzdvds  15547  powm2modprm  15555  modprmn0modprm0  15559  coprimeprodsq  15560  pythagtriplem1  15568  pythagtriplem4  15571  pc2dvds  15630  pc11  15631  pcz  15632  pcprod  15646  prmunb  15665  1arithlem3  15676  1arith  15678  cshwshashlem2  15850  cshwshashlem3  15851  ressabs  15986  acsfn2  16371  issect  16460  funcestrcsetclem9  16835  funcsetcestrclem5  16846  funcsetcestrclem9  16850  pospo  17020  latjcom  17106  latmcom  17122  clatglbss  17174  pospropd  17181  pslem  17253  tsrss  17270  issubmnd  17365  submcl  17400  resmhm2b  17408  frmdmnd  17443  frmd0  17444  grpinvsub  17544  dfgrp3lem  17560  gimcnv  17756  gimco  17757  gictr  17764  cntz2ss  17811  cntzrec  17812  symg2bas  17864  symgextf1  17887  symgfixelsi  17901  pmtrfinv  17927  pmtrdifwrdel2  17952  dfod2  18027  lsmcom2  18116  efgred  18207  qusabl  18314  cygabl  18338  gsummptnn0fz  18428  eldprd  18449  srgmulgass  18577  dfrhm2  18765  isrim0  18771  rmodislmodlem  18978  rmodislmod  18979  lmimcnv  19115  mplcoe5lem  19515  psrbagfsupp  19557  cnfldexp  19827  cnsrng  19828  xrsdsreval  19839  dvdsrzring  19879  znf1o  19948  ocvocv  20063  ocvin  20066  frlmip  20165  islindf  20199  lindff  20202  lindfrn  20208  f1lindf  20209  mamudir  20258  matsca2  20274  matbas2  20275  matlmod  20283  matinvgcell  20289  mat1bas  20303  dmatmul  20351  dmatsgrp  20353  dmatsrng  20355  dmatcrng  20356  scmatsgrp1  20376  scmatsrng1  20377  madulid  20499  gsummatr01lem3  20511  gsummatr01  20513  cpmatacl  20569  0mat2pmat  20589  idmatidpmat  20590  m2cpminv0  20614  pmatcollpw3fi1lem1  20639  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  eltg  20809  eltg2  20810  tgss  20820  tgss2  20839  basgen2  20841  bastop1  20845  cldmre  20930  toponmre  20945  opnneiss  20970  restcldr  21026  restfpw  21031  restcls  21033  restntr  21034  ordtbaslem  21040  ordtrest2lem  21055  leordtvallem2  21063  leordtval  21065  cnrest  21137  t0sep  21176  cmpcov  21240  cmpsublem  21250  cmpsub  21251  bwth  21261  2ndcomap  21309  locfincmp  21377  ptval  21421  xkoval  21438  txss12  21456  ptrescn  21490  xkopt  21506  hmeofval  21609  txswaphmeolem  21655  txswaphmeo  21656  trfbas2  21694  trfbas  21695  uzrest  21748  numufl  21766  ssufl  21769  flimclsi  21829  hauspwpwf1  21838  ghmcnp  21965  blpnfctr  22288  metequiv  22361  metcnp3  22392  elbl4  22415  restmetu  22422  tngngp  22505  qtopbaslem  22609  bl2ioo  22642  ioo2bl  22643  ioo2blex  22644  xrsxmet  22659  divccn  22723  divccncf  22756  isclmi0  22944  iscvsi  22975  causs  23142  lmclim  23147  bcthlem1  23167  ovolfsf  23286  ioombl  23379  iccvolcl  23381  ioovolcl  23384  ioorcl  23391  volcn  23420  itg2itg1  23548  dvexp  23761  dvmptfsum  23783  dvexp3  23786  dvef  23788  dvlip  23801  c1lip1  23805  ftc1a  23845  tdeglem1  23863  tdeglem3  23864  tdeglem4  23865  coe1termlem  24059  plyremlem  24104  ptolemy  24293  cos11  24324  logeftb  24375  logleb  24394  logdivlt  24412  logdivle  24413  angval  24576  isppw2  24886  issqf  24907  vmasum  24986  lgsprme0  25109  gausslemma2dlem1a  25135  lgsquadlem3  25152  2lgsoddprmlem2  25179  ostth  25373  brbtwn2  25830  colinearalglem4  25834  ax5seglem1  25853  ax5seglem2  25854  axcontlem2  25890  axcontlem12  25900  upgrpredgv  26079  uhgr2edg  26145  issubgr  26208  subgrprop  26210  subuhgr  26223  subupgr  26224  subumgr  26225  subusgr  26226  nb3grprlem2  26327  cplgr3v  26387  wlk1walk  26591  upgrwlkvtxedg  26597  pthdivtx  26681  usgr2trlncl  26712  crctcshwlkn0lem3  26760  crctcshwlkn0lem6  26763  crctcshwlkn0lem7  26764  crctcshwlkn0  26769  wlkiswwlks2  26829  wwlksnextbi  26857  wwlksnfi  26869  wwlksnextprop  26875  erclwwlksym  26978  clwwlkn1  27004  clwwlkfo  27013  clwwlknwwlknclOLD  27017  erclwwlknsym  27034  clwwlknonex2lem2  27083  is0wlk  27095  is0trl  27101  3pthdlem1  27142  frgr3v  27255  frgrncvvdeqlem3  27281  frgrregorufr  27305  2clwwlk2clwwlklem2lem2  27329  numclwwlk1  27351  numclwlk2lem2f  27357  numclwlk2lem2f1o  27359  numclwlk2lem2fOLD  27364  numclwlk2lem2f1oOLD  27366  frgrregord013  27382  vcz  27558  isvcOLD  27562  isnv  27595  isnvi  27596  nmooge0  27750  nmblolbii  27782  blocnilem  27787  ipblnfi  27839  hvpncan2  28025  hvaddsub4  28063  hire  28079  abshicom  28086  hial2eq2  28092  orthcom  28093  hhssabloi  28247  ocsh  28270  shscli  28304  shscom  28306  shsel2  28309  spanss  28335  shjcom  28345  shmodsi  28376  chpsscon3  28490  spansni  28544  spansnmul  28551  spansncol  28555  spanunsni  28566  cmcm2  28603  cm2j  28607  spansncvi  28639  5oalem2  28642  3oalem2  28650  honegsubdi2  28798  adjsym  28820  cnvadj  28879  brafn  28934  kbpj  28943  riesz3i  29049  cnlnadjlem2  29055  cnlnadjlem9  29062  nmopcoi  29082  cnvbraval  29097  leop  29110  leop3  29112  leopmul2i  29122  leoptri  29123  hstrlem3a  29247  cvcon3  29271  cvnsym  29277  mdbr2  29283  dmdmd  29287  dmdbr2  29290  dmdbr3  29292  dmdbr4  29293  dmdbr5  29295  mdsl0  29297  ssmd2  29299  mdslmd1lem1  29312  mdslmd1lem2  29313  mdslmd3i  29319  mdslmd4i  29320  atcveq0  29335  superpos  29341  atnemeq0  29364  atssma  29365  atexch  29368  atomli  29369  atcvatlem  29372  atcvati  29373  chirredlem1  29377  chirredlem3  29379  chirredi  29381  atcvat3i  29383  atdmd  29385  mdsymlem1  29390  mdsymlem3  29392  mdsymlem4  29393  mdsymlem5  29394  mdsymlem8  29397  dmdsym  29400  atdmd2  29401  sumdmdlem  29405  cdjreui  29419  cdj3lem2b  29424  cdj3i  29428  r19.29ffa  29448  imadifxp  29540  abfmpel  29583  xaddeq0  29646  xrofsup  29661  xeqlelt  29666  xdivpnfrp  29769  xrsinvgval  29805  xrsmulgzz  29806  pcmplfin  30055  cnvordtrestixx  30087  ordtrest2NEWlem  30096  indval  30203  esumpfinvallem  30264  sigagenss  30340  ddemeas  30427  brae  30432  dya2iocival  30463  dya2iocnei  30472  dya2iocuni  30473  omsf  30486  oddpwdc  30544  bnj934  31131  derangenlem  31279  subfacval2  31295  kur14  31324  lediv2aALT  31697  dford5  31734  faclim2  31760  funpsstri  31789  dftrpred3g  31857  soseq  31879  wsuclem  31895  frrlem5  31909  elno  31924  nosepon  31943  noextenddif  31946  sltsolem1  31951  nosepne  31956  nolt02o  31970  sltnle  32003  sleloe  32004  sletri3  32005  hfelhf  32413  elicc3  32436  nn0prpwlem  32442  nn0prpw  32443  isfne  32459  onsuct0  32565  nndivsub  32581  bj-ssbequ2  32768  bj-restsnss  33161  bj-restsnss2  33162  bj-restuni2  33176  topdifinffinlem  33325  iooelexlt  33340  relowlssretop  33341  rdgeqoa  33348  wl-sbcom2d-lem1  33472  wl-sbcom2d  33474  wl-ax11-lem6  33497  curf  33517  finixpnum  33524  ltflcei  33527  leceifl  33528  cos2h  33530  matunitlindflem1  33535  matunitlindflem2  33536  matunitlindf  33537  ptrecube  33539  poimirlem6  33545  poimirlem7  33546  poimirlem10  33549  poimirlem11  33550  poimirlem27  33566  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  cnambfre  33588  itg2addnclem2  33592  itg2addnc  33594  itg2gt0cn  33595  ftc1anclem1  33615  ftc1anclem4  33618  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anc  33623  unirep  33637  opelopab3  33641  fvopabf4g  33645  indexa  33658  filbcmb  33665  incsequz2  33675  metf1o  33681  sstotbnd3  33705  isbnd2  33712  bndss  33715  ismtycnv  33731  iccbnd  33769  exidreslem  33806  exidresid  33808  ghomco  33820  isdivrngo  33879  isdrngo2  33887  rngoisocnv  33910  riscer  33917  crngohomfo  33935  unichnidl  33960  maxidlmax  33972  igenmin  33993  exmid2  34031  orel  34034  brcosscnvcoss  34329  brssr  34391  prtlem16  34473  paddss1  35421  paddss2  35422  paddss12  35423  pclfinN  35504  erngmul-rN  36419  mapdordlem2  37243  ismrc  37581  nacsfg  37585  isnacs3  37590  incssnn0  37591  mzpclall  37607  lerabdioph  37686  ltrabdioph  37689  eldioph4b  37692  jm2.17b  37845  congrep  37857  lnr2i  38003  rp-fakenanass  38177  brnonrel  38212  enrelmap  38608  enrelmapr  38609  rcompleq  38635  isotone1  38663  isotone2  38664  radcnvrat  38830  expgrowth  38851  bcc0  38856  binomcxplemnn0  38865  2sbc6g  38933  2sbc5g  38934  ordpss  38972  addrcom  38996  3impcombi  39361  sspwimp  39468  sspwimpVD  39469  ax6e2ndeqALT  39481  iunconnlem2  39485  sineq0ALT  39487  nsstr  39587  iunmapsn  39723  ssfiunibd  39837  fmul01  40130  lptre2pt  40190  stoweidlem34  40569  dirkeritg  40637  fourierdlem73  40714  smfsuplem1  41338  smfinflem  41344  sigarac  41362  2reu3  41509  afv0nbfvbi  41552  dmfcoafv  41576  cnambpcma  41634  ltnltne  41638  fzoopth  41662  elmod2  41665  pfxccatin12lem1  41748  pfxccatin12lem2  41749  pfxccatin12  41750  fmtnofac2lem  41805  prmdvdsfmtnof1lem2  41822  proththd  41856  opoeALTV  41919  opeoALTV  41920  epoo  41937  evenprm2  41948  gbegt5  41974  sbgoldbaltlem2  41993  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  bgoldbtbndlem4  42021  bgoldbtbnd  42022  sprsymrelfolem2  42068  sprsymrelf1  42071  uspgrsprfo  42081  submgmcl  42119  resmgmhm2b  42125  isassintop  42171  rnghmval  42216  isrngisom  42221  c0snghm  42241  zrrnghm  42242  2zrngamgm  42264  rnghmsubcsetclem2  42301  rhmsubcsetclem2  42347  rhmsubcrngclem1  42352  rhmsubcrngclem2  42353  funcringcsetcALTV2lem9  42369  funcringcsetclem9ALTV  42392  rhmsubclem4  42414  rhmsubcALTVlem4  42432  cbvmpt2x2  42439  nn0sumltlt  42453  gsumlsscl  42489  ply1mulgsumlem1  42499  lincvalpr  42532  lincdifsn  42538  linc1  42539  lincellss  42540  islinindfiss  42564  islindeps  42567  lincresunit2  42592  islininds2  42598  lmod1zr  42607  ltsubadd2b  42631  zgtp1leeq  42636  logblt1b  42683  blengt1fldiv2p1  42712  nn0sumshdiglemB  42739  aacllem  42875
  Copyright terms: Public domain W3C validator