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

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
StepHypRef Expression
1 ancoms.1 . . 3 ((𝜑𝜓) → 𝜒)
21expcom 451 . 2 (𝜓 → (𝜑𝜒))
32imp 445 1 ((𝜓𝜑) → 𝜒)
Colors of variables: wff setvar class
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  590  sylan9bbr  736  anabss4  855  anabsi7  859  anabsi8  860  im2anan9r  880  bi2anan9r  917  syl3anr2  1376  mp3anr1  1418  mp3anr2  1419  mp3anr3  1420  stoic1b  1695  dvelimf  2333  2eu3  2554  eqeqan12rd  2639  sylan9eqr  2677  r19.29vva  3075  morex  3377  sbcrext  3498  sbcrextOLD  3499  sylan9ssr  3602  pssdifcom1  4032  pssdifcom2  4033  riinn0  4568  breqan12rd  4640  propeqop  4940  soinxp  5154  frinxp  5155  seinxp  5156  brelrng  5325  dminss  5516  imainss  5517  sossfld  5549  setlikespec  5670  ordelssne  5719  ordtri3or  5724  ordtri2  5727  ordtri4  5730  ordtr3OLD  5739  ordtri2or  5791  funsng  5905  f1co  6077  f1ocnv  6116  f1oprswap  6147  funimass4  6214  dffv2  6238  fndmdifcom  6288  fsn2  6368  fvtp2  6426  fvtp3  6427  fvtp2g  6429  fvtp3g  6430  soisoi  6543  riotaeqimp  6599  oveqan12rd  6635  brrpssg  6904  sorpsscmpl  6913  dfwe2  6943  ordsucelsuc  6984  ordunisuc2  7006  tfindsg  7022  tfindsg2  7023  dfom2  7029  funcnvuni  7081  fun11iun  7088  cofunex2g  7093  curry2  7232  soxp  7250  mpt2xopoveqd  7307  tposoprab  7348  wfr3g  7373  wfrlem5  7379  wfrlem10  7384  smores3  7410  smores2  7411  smoel  7417  dfrecs3  7429  tfr3  7455  tz7.48-2  7497  tz7.49  7500  oaordi  7586  oaword  7589  oaord1  7591  oaword2  7593  oa00  7599  oalimcl  7600  oaass  7601  oarec  7602  oacomf1o  7605  omord2  7607  omcan  7609  omword  7610  omword1  7613  omword2  7614  odi  7619  omass  7620  oneo  7621  oen0  7626  oecan  7629  oelim2  7635  nnarcl  7656  nnaordi  7658  nnaordr  7660  nnawordi  7661  nnmsucr  7665  nnmcom  7666  nnaword  7667  nnmordi  7671  nnaordex  7678  oaabslem  7683  omabslem  7686  nnneo  7691  omsmo  7694  ersym  7714  elecg  7745  riiner  7780  ecopovsym  7809  ecovcom  7814  mapvalg  7827  pmvalg  7828  elpmg  7833  elmapssres  7842  pmss12g  7844  ixpconstg  7877  ener  7962  enerOLD  7963  domtr  7969  f1imaeng  7976  fundmen  7990  xpcomco  8010  xpsnen2g  8013  xpdom2  8015  xpdom1g  8017  omxpen  8022  omf1o  8023  enen2  8061  domen2  8063  sdomen2  8065  domtriord  8066  sdomel  8067  onsdominel  8069  infensuc  8098  onomeneq  8110  nndomo  8114  pssnn  8138  unbnn  8176  infcntss  8194  fiint  8197  mapfi  8222  fiin  8288  fiss  8290  infempty  8372  oiiso  8402  unwdomg  8449  suc11reg  8476  inf3lem5  8489  infeq5  8494  cantnfp1lem3  8537  r1tr  8599  r1val1  8609  rankr1ai  8621  rankonidlem  8651  onssr1  8654  tskwe  8736  carddom2  8763  carden2  8773  domtri2  8775  cardval2  8777  fidomtri  8779  fidomtri2  8780  harval2  8783  dif1card  8793  infxpenlem  8796  ac5num  8819  alephord3  8861  alephdom  8864  aleph11  8867  alephdom2  8870  cardaleph  8872  dfac3  8904  dfac5  8911  cdacomen  8963  onacda  8979  pwsdompw  8986  ackbij1lem11  9012  ackbij2  9025  cfeq0  9038  cfsuc  9039  cff1  9040  cflim2  9045  cfsmolem  9052  coftr  9055  sornom  9059  infpssrlem4  9088  ssfin4  9092  ssfin2  9102  ssfin3ds  9112  fin23lem31  9125  isf32lem9  9143  hsmexlem5  9212  axdc3lem  9232  axdc3lem2  9233  axdc3lem4  9235  zorn2lem6  9283  brdom3  9310  brdom7disj  9313  brdom6disj  9314  alephval2  9354  alephreg  9364  wuncss  9527  gruen  9594  addcompi  9676  mulcompi  9678  ltapi  9685  ltmpi  9686  nqereu  9711  addcompq  9732  addcomnq  9733  mulcompq  9734  mulcomnq  9735  ltsonq  9751  ltanq  9753  ltmnq  9754  genpnnp  9787  addcompr  9803  mulcompr  9805  ltsopr  9814  ltexprlem2  9819  prlem936  9829  suplem2pr  9835  map2psrpr  9891  axpre-ltadd  9948  xrltnle  10065  axlttri  10069  axsup  10073  ltnle  10077  letri3  10083  leloe  10084  eqlelt  10085  letric  10097  mul31  10164  subcl  10240  pncan2  10248  pncan3  10249  npcan  10250  addsubeq4  10256  npncan3  10279  negsubdi2  10300  muladd  10422  subdi  10423  mulneg2  10427  mulsub  10433  ltleadd  10471  ltsubpos  10480  posdif  10481  addge01  10498  lesub0  10505  wloglei  10520  prodgt02  10829  prodge02  10831  mulsuble0b  10855  ltdivmul  10858  ledivmul  10859  lt2mul2div  10861  lerec  10866  lt2msq  10868  ltdiv23  10874  lediv23  10875  lediv2a  10877  le2msq  10883  msq11  10884  fimaxre  10928  lbreu  10933  infm3  10942  dfinfre  10964  creur  10974  creui  10975  cju  10976  nnmulcl  11003  nndivtr  11022  avgle1  11232  avgle2  11233  avgle  11234  nn0nnaddcl  11284  ltsubnn0  11304  zrevaddcl  11382  znnsub  11383  znn0sub  11384  zextlt  11411  gtndiv  11414  prime  11418  uztrn2  11665  uztric  11669  uz11  11670  nn0pzuz  11705  uzwo  11711  zmax  11745  zbtwnre  11746  rebtwnz  11747  qrevaddcl  11770  rpnnen1lem2  11774  rpnnen1lem1  11775  rpnnen1lem3  11776  rpnnen1lem5  11778  rpnnen1lem1OLD  11781  rpnnen1lem3OLD  11782  rpnnen1lem5OLD  11784  difrp  11828  xrltnsym  11930  xrlttri  11932  xrleloe  11937  xrletri  11944  xrletri3  11945  xrmaxeq  11969  xrmineq  11970  xrmaxlt  11971  xrmaxle  11973  lemaxle  11985  z2ge  11988  qbtwnre  11989  qextlt  11993  qextle  11994  xleneg  12008  xaddcom  12030  xmulcom  12055  xmulneg2  12059  xmulgt0  12072  xrsupsslem  12096  xrinfmsslem  12097  supxrunb1  12108  supxrunb2  12109  ixxssixx  12147  ixxin  12150  ioon0  12159  iccid  12178  iooshf  12210  iccsupr  12224  iooneg  12250  iccneg  12251  iccsplit  12263  fzen  12316  fzadd2  12334  fzass4  12337  fzrev  12361  fznn  12366  elfzp1b  12374  elfzm1b  12375  fz0fzdiffz0  12405  difelfznle  12410  fzon  12446  fzo0n  12447  fzonmapblen  12470  elfzoext  12481  eluzgtdifelfzo  12486  ubmelm1fzo  12521  elfzom1elp1fzo1  12525  subfzo0  12546  fllt  12563  flflp1  12564  flbi  12573  flbi2  12574  flzadd  12583  ltdifltdiv  12591  dfceil2  12596  modcyc2  12662  modifeq2int  12688  modaddmodup  12689  modaddmodlo  12690  modfzo0difsn  12698  modsumfzodifsn  12699  om2uzlt2i  12706  om2uzf1oi  12708  fseqsupubi  12733  fsuppmapnn0fiub0  12749  expcllem  12827  mulbinom2  12940  faclbnd5  13041  hashbnd  13079  hasheni  13092  hasheqf1oi  13096  hasheqf1oiOLD  13097  hashdom  13124  hashss  13153  hashfacen  13192  ccatsymb  13321  ccatass  13326  ccatalpha  13330  wrd2ind  13431  swrdccatin12lem2b  13439  swrdccatin2  13440  swrdccatin12lem2  13442  swrdccatin12  13444  swrdccat3blem  13448  swrdccatid  13450  repswsymball  13479  repswsymballbi  13480  cshwsublen  13495  cshwn  13496  cshwlen  13498  cshwidxmod  13502  cshf1  13509  repswcshw  13511  cshweqdif2  13518  cshweqrep  13520  cshwcsh2id  13527  ccatco  13534  swrdco  13536  lswco  13537  s3iunsndisj  13657  relexprelg  13728  relexpnndm  13731  relexpaddnn  13741  shftlem  13758  shftuz  13759  shftfval  13760  shftval4  13767  shftval5  13768  2shfti  13770  seqshft  13775  mulre  13811  sqrtlt  13952  abs3dif  14021  abs2difabs  14024  uzin2  14034  rexanre  14036  caubnd  14048  climshftlem  14255  rlimcn2  14271  fsumcnv  14451  modfsummods  14471  geo2lim  14550  ntrivcvgfvn0  14575  prodmo  14610  zprod  14611  prodss  14621  fprodcnv  14657  bpolysum  14728  bpoly4  14734  efle  14792  reef11  14793  demoivre  14874  demoivreALT  14875  znnenlem  14884  sqrt2irr  14922  nndivides  14933  0dvds  14945  muldvds1  14949  muldvds2  14950  dvdscmulr  14953  dvdssubr  14970  dvdsadd2b  14971  odd2np1  15008  mulsucdiv2z  15020  ltoddhalfle  15028  divalglem9  15067  ndvdssub  15076  gcdcllem1  15164  gcdcom  15178  neggcd  15187  gcdabs2  15195  modgcd  15196  lcmcom  15249  neglcm  15260  lcmgcdeq  15268  coprmdvds  15309  coprmdvdsOLD  15310  qredeq  15314  divgcdcoprmex  15323  dvdsprm  15358  cncongrprm  15380  odzdvds  15443  powm2modprm  15451  modprmn0modprm0  15455  coprimeprodsq  15456  pythagtriplem1  15464  pythagtriplem4  15467  pc2dvds  15526  pc11  15527  pcz  15528  pcprod  15542  prmunb  15561  1arithlem3  15572  1arith  15574  cshwshashlem2  15746  cshwshashlem3  15747  ressabs  15879  acsfn2  16264  issect  16353  funcestrcsetclem9  16728  funcsetcestrclem5  16739  funcsetcestrclem9  16743  pospo  16913  latjcom  16999  latmcom  17015  clatglbss  17067  pospropd  17074  pslem  17146  tsrss  17163  issubmnd  17258  submcl  17293  resmhm2b  17301  frmdmnd  17336  frmd0  17337  grpinvsub  17437  dfgrp3lem  17453  gimcnv  17649  gimco  17650  gictr  17657  cntz2ss  17705  cntzrec  17706  symg2bas  17758  symgextf1  17781  symgfixelsi  17795  pmtrfinv  17821  pmtrdifwrdel2  17846  dfod2  17921  lsmcom2  18010  efgred  18101  qusabl  18208  cygabl  18232  gsummptnn0fz  18322  eldprd  18343  srgmulgass  18471  dfrhm2  18657  isrim0  18663  rmodislmodlem  18870  rmodislmod  18871  lmimcnv  19007  mplcoe5lem  19407  psrbagfsupp  19449  cnfldexp  19719  cnsrng  19720  xrsdsreval  19731  dvdsrzring  19771  znf1o  19840  ocvocv  19955  ocvin  19958  frlmip  20057  islindf  20091  lindff  20094  lindfrn  20100  f1lindf  20101  mamudir  20150  matsca2  20166  matbas2  20167  matlmod  20175  matinvgcell  20181  mat1bas  20195  dmatmul  20243  dmatsgrp  20245  dmatsrng  20247  dmatcrng  20248  scmatsgrp1  20268  scmatsrng1  20269  madulid  20391  gsummatr01lem3  20403  gsummatr01  20405  cpmatacl  20461  0mat2pmat  20481  idmatidpmat  20482  m2cpminv0  20506  pmatcollpw3fi1lem1  20531  chfacfscmulgsum  20605  chfacfpmmulgsum  20609  eltg  20701  eltg2  20702  tgss  20712  tgss2  20731  basgen2  20733  bastop1  20737  cldmre  20822  toponmre  20837  opnneiss  20862  restcldr  20918  restfpw  20923  restcls  20925  restntr  20926  ordtbaslem  20932  ordtrest2lem  20947  leordtvallem2  20955  leordtval  20957  cnrest  21029  t0sep  21068  cmpcov  21132  cmpsublem  21142  cmpsub  21143  bwth  21153  2ndcomap  21201  locfincmp  21269  ptval  21313  xkoval  21330  txss12  21348  ptrescn  21382  xkopt  21398  hmeofval  21501  txswaphmeolem  21547  txswaphmeo  21548  trfbas2  21587  trfbas  21588  uzrest  21641  numufl  21659  ssufl  21662  flimclsi  21722  hauspwpwf1  21731  ghmcnp  21858  blpnfctr  22181  metequiv  22254  metcnp3  22285  elbl4  22308  restmetu  22315  tngngp  22398  qtopbaslem  22502  bl2ioo  22535  ioo2bl  22536  ioo2blex  22537  xrsxmet  22552  divccn  22616  divccncf  22649  isclmi0  22838  iscvsi  22869  causs  23036  lmclim  23041  bcthlem1  23061  ovolfsf  23180  ioombl  23273  iccvolcl  23275  ioovolcl  23278  ioorcl  23285  volcn  23314  itg2itg1  23443  dvexp  23656  dvmptfsum  23676  dvexp3  23679  dvef  23681  dvlip  23694  c1lip1  23698  ftc1a  23738  tdeglem1  23756  tdeglem3  23757  tdeglem4  23758  coe1termlem  23952  plyremlem  23997  ptolemy  24186  cos11  24217  logeftb  24268  logleb  24287  logdivlt  24305  logdivle  24306  angval  24465  isppw2  24775  issqf  24796  vmasum  24875  lgsprme0  24998  gausslemma2dlem1a  25024  lgsquadlem3  25041  2lgsoddprmlem2  25068  ostth  25262  brbtwn2  25719  colinearalglem4  25723  ax5seglem1  25742  ax5seglem2  25743  axcontlem2  25779  axcontlem12  25789  upgrpredgv  25963  uhgr2edg  26027  issubgr  26090  subgrprop  26092  subuhgr  26105  subupgr  26106  subumgr  26107  subusgr  26108  nb3grprlem2  26204  cplgr3v  26252  wlk1walk  26438  upgrwlkvtxedg  26444  pthdivtx  26528  usgr2trlncl  26559  crctcshwlkn0lem3  26607  crctcshwlkn0lem6  26610  crctcshwlkn0lem7  26611  crctcshwlkn0  26616  wlkiswwlks2  26664  wwlksnextbi  26692  wwlksnfi  26704  wwlksnextprop  26710  clwwlksfo  26818  erclwwlkssym  26835  erclwwlksnsym  26847  is0wlk  26878  is0trl  26884  3pthdlem1  26924  frgr3v  27037  frgrregorufr  27082  numclwwlkovfel2  27106  numclwwlk1  27120  numclwlk2lem2f  27125  numclwlk2lem2f1o  27127  frgrregord013  27141  vcz  27318  isvcOLD  27322  isnv  27355  isnvi  27356  nmooge0  27510  nmblolbii  27542  blocnilem  27547  ipblnfi  27599  hvpncan2  27785  hvaddsub4  27823  hire  27839  abshicom  27846  hial2eq2  27852  orthcom  27853  hhssabloi  28007  ocsh  28030  shscli  28064  shscom  28066  shsel2  28069  spanss  28095  shjcom  28105  shmodsi  28136  chpsscon3  28250  spansni  28304  spansnmul  28311  spansncol  28315  spanunsni  28326  cmcm2  28363  cm2j  28367  spansncvi  28399  5oalem2  28402  3oalem2  28410  honegsubdi2  28558  adjsym  28580  cnvadj  28639  brafn  28694  kbpj  28703  riesz3i  28809  cnlnadjlem2  28815  cnlnadjlem9  28822  nmopcoi  28842  cnvbraval  28857  leop  28870  leop3  28872  leopmul2i  28882  leoptri  28883  hstrlem3a  29007  cvcon3  29031  cvnsym  29037  mdbr2  29043  dmdmd  29047  dmdbr2  29050  dmdbr3  29052  dmdbr4  29053  dmdbr5  29055  mdsl0  29057  ssmd2  29059  mdslmd1lem1  29072  mdslmd1lem2  29073  mdslmd3i  29079  mdslmd4i  29080  atcveq0  29095  superpos  29101  atnemeq0  29124  atssma  29125  atexch  29128  atomli  29129  atcvatlem  29132  atcvati  29133  chirredlem1  29137  chirredlem3  29139  chirredi  29141  atcvat3i  29143  atdmd  29145  mdsymlem1  29150  mdsymlem3  29152  mdsymlem4  29153  mdsymlem5  29154  mdsymlem8  29157  dmdsym  29160  atdmd2  29161  sumdmdlem  29165  cdjreui  29179  cdj3lem2b  29184  cdj3i  29188  r19.29ffa  29208  imadifxp  29300  abfmpel  29338  xaddeq0  29402  xrofsup  29418  xeqlelt  29423  xdivpnfrp  29468  xrsinvgval  29504  xrsmulgzz  29505  pcmplfin  29751  cnvordtrestixx  29783  ordtrest2NEWlem  29792  indval  29899  esumpfinvallem  29959  sigagenss  30035  ddemeas  30122  brae  30127  dya2iocival  30158  dya2iocnei  30167  dya2iocuni  30168  omsf  30181  oddpwdc  30239  bnj934  30766  derangenlem  30914  subfacval2  30930  kur14  30959  lediv2aALT  31332  dford5  31370  faclim2  31395  funpsstri  31420  dftrpred3g  31487  soseq  31505  wsuclem  31527  wsuclemOLD  31528  frrlem5  31538  elno  31553  nosepon  31576  noextenddif  31578  sltsolem1  31581  slttr2  31588  slttr3  31589  nodenselem4  31600  nosepne  31619  hfelhf  31983  elicc3  32006  nn0prpwlem  32012  nn0prpw  32013  isfne  32029  onsuct0  32135  nndivsub  32151  bj-ssbequ2  32338  bj-restsnss  32726  bj-restsnss2  32727  bj-restuni2  32741  topdifinffinlem  32866  iooelexlt  32881  relowlssretop  32882  rdgeqoa  32889  wl-sbcom2d-lem1  33013  wl-sbcom2d  33015  wl-ax11-lem6  33038  curf  33058  finixpnum  33065  ltflcei  33068  leceifl  33069  cos2h  33071  matunitlindflem1  33076  matunitlindflem2  33077  matunitlindf  33078  ptrecube  33080  poimirlem6  33086  poimirlem7  33087  poimirlem10  33090  poimirlem11  33091  poimirlem27  33107  poimirlem29  33109  poimirlem30  33110  poimirlem31  33111  poimirlem32  33112  mblfinlem3  33119  mblfinlem4  33120  ismblfin  33121  ovoliunnfl  33122  voliunnfl  33124  volsupnfl  33125  cnambfre  33129  itg2addnclem2  33133  itg2addnc  33135  itg2gt0cn  33136  ftc1anclem1  33156  ftc1anclem4  33159  ftc1anclem6  33161  ftc1anclem7  33162  ftc1anc  33164  unirep  33178  opelopab3  33182  fvopabf4g  33186  indexa  33199  filbcmb  33206  incsequz2  33216  metf1o  33222  sstotbnd3  33246  isbnd2  33253  bndss  33256  ismtycnv  33272  iccbnd  33310  exidreslem  33347  exidresid  33349  ghomco  33361  isdivrngo  33420  isdrngo2  33428  rngoisocnv  33451  riscer  33458  crngohomfo  33476  unichnidl  33501  maxidlmax  33513  igenmin  33534  exmid2  33572  orel  33575  prtlem16  33673  paddss1  34622  paddss2  34623  paddss12  34624  pclfinN  34705  erngmul-rN  35621  mapdordlem2  36445  ismrc  36783  nacsfg  36787  isnacs3  36792  incssnn0  36793  mzpclall  36809  lerabdioph  36888  ltrabdioph  36891  eldioph4b  36894  jm2.17b  37047  congrep  37059  lnr2i  37206  rp-fakenanass  37380  brnonrel  37415  enrelmap  37812  enrelmapr  37813  rcompleq  37839  isotone1  37867  isotone2  37868  radcnvrat  38034  expgrowth  38055  bcc0  38060  binomcxplemnn0  38069  2sbc6g  38137  2sbc5g  38138  ordpss  38176  addrcom  38200  3impcombi  38565  sspwimp  38676  sspwimpVD  38677  ax6e2ndeqALT  38689  iunconnlem2  38693  sineq0ALT  38695  nsstr  38795  iunmapsn  38918  ssfiunibd  39022  fmul01  39248  lptre2pt  39308  stoweidlem34  39588  dirkeritg  39656  fourierdlem73  39733  smfsuplem1  40354  smfinflem  40360  sigarac  40375  2reu3  40522  afv0nbfvbi  40565  dmfcoafv  40589  cnambpcma  40636  ltnltne  40640  fzoopth  40664  elmod2  40668  pfxccatin12lem1  40752  pfxccatin12lem2  40753  pfxccatin12  40754  fmtnofac2lem  40809  prmdvdsfmtnof1lem2  40826  proththd  40860  opoeALTV  40923  opeoALTV  40924  epoo  40941  evenprm2  40952  gbegt5  40974  sgoldbaltlem2  40993  nnsum4primeseven  41007  nnsum4primesevenALTV  41008  bgoldbtbndlem4  41015  bgoldbtbnd  41016  sprsymrelfolem2  41061  sprsymrelf1  41064  uspgrsprfo  41074  submgmcl  41112  resmgmhm2b  41118  isassintop  41164  rnghmval  41209  isrngisom  41214  c0snghm  41234  zrrnghm  41235  2zrngamgm  41257  rnghmsubcsetclem2  41294  rhmsubcsetclem2  41340  rhmsubcrngclem1  41345  rhmsubcrngclem2  41346  funcringcsetcALTV2lem9  41362  funcringcsetclem9ALTV  41385  rhmsubclem4  41407  rhmsubcALTVlem4  41425  cbvmpt2x2  41432  nn0sumltlt  41446  gsumlsscl  41482  ply1mulgsumlem1  41492  lincvalpr  41525  lincdifsn  41531  linc1  41532  lincellss  41533  islinindfiss  41557  islindeps  41560  lincresunit2  41585  islininds2  41591  lmod1zr  41600  ltsubadd2b  41624  zgtp1leeq  41629  logblt1b  41680  blengt1fldiv2p1  41709  nn0sumshdiglemB  41736  aacllem  41880
  Copyright terms: Public domain W3C validator