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

Theorem ancoms 440
Description: Inference commuting conjunction in antecedent. (Contributed by NM, 21-Apr-1994.)
Hypothesis
Ref Expression
ancoms.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
ancoms  |-  ( ( ps  /\  ph )  ->  ch )

Proof of Theorem ancoms
StepHypRef Expression
1 ancoms.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21expcom 425 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32imp 419 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  adantl  453  syl2anr  465  anim12ci  551  sylan9bbr  682  anabss4  789  anabsi7  793  anabsi8  794  im2anan9r  810  bi2anan9r  845  syl3anr2  1237  mp3anr1  1276  mp3anr2  1277  mp3anr3  1278  19.29r  1607  dvelimf  2064  nfeud2  2292  2eu1  2360  2eu3  2362  eqeqan12rd  2451  sylan9eqr  2489  r19.29_2a  2844  morex  3110  sbcrext  3226  sylan9ssr  3354  pssdifcom1  3705  pssdifcom2  3706  riinn0  4157  breqan12rd  4220  ordelssne  4600  ordtri3or  4605  ordtri2  4608  ordtri4  4610  ordtr2  4617  ordtr3  4618  ordintdif  4622  ordtri2or  4669  dfwe2  4754  ordsucelsuc  4794  ordunisuc2  4816  tfindsg  4832  tfindsg2  4833  dfom2  4839  soinxp  4934  frinxp  4935  seinxp  4936  brelrng  5091  dminss  5278  imainss  5279  funsng  5489  funcnvuni  5510  f1co  5640  f1ocnv  5679  fun11iun  5687  f1oprswap  5709  funimass4  5769  dffv2  5788  fndmdifcom  5827  fsn2  5900  fvtp2  5932  fvtp3  5933  fvtp2g  5935  fvtp3g  5936  cofunex2g  5952  soisoi  6040  oveqan12rd  6093  curry2  6433  soxp  6451  mpt2xopoveqd  6464  tposoprab  6507  brrpssg  6516  sorpsscmpl  6525  smores3  6607  smores2  6608  smoel  6614  tfr3  6652  tz7.48-2  6691  tz7.49  6694  oaordi  6781  oaword  6784  oaord1  6786  oaword2  6788  oa00  6794  oalimcl  6795  oaass  6796  oarec  6797  oacomf1o  6800  omord2  6802  omcan  6804  omword  6805  omword1  6808  omword2  6809  odi  6814  omass  6815  oneo  6816  oen0  6821  oecan  6824  oelim2  6830  nnarcl  6851  nnaordi  6853  nnaordr  6855  nnawordi  6856  nnmsucr  6860  nnmcom  6861  nnaword  6862  nnmordi  6866  nnaordex  6873  oaabslem  6878  omabslem  6881  nnneo  6886  omsmo  6889  ersym  6909  elecg  6935  riiner  6969  ecopovsym  6998  ecovcom  7007  mapvalg  7020  pmvalg  7021  elpmg  7024  pmss12g  7032  ixpconstg  7063  ener  7146  domtr  7152  f1imaeng  7159  fundmen  7172  xpcomco  7190  xpsnen2g  7193  xpdom2  7195  xpdom1g  7197  omxpen  7202  omf1o  7203  enen2  7240  domen2  7242  sdomen2  7244  domtriord  7245  sdomel  7246  onsdominel  7248  infensuc  7277  onomeneq  7288  nndomo  7292  pssnn  7319  unbnn  7355  infcntss  7372  fiint  7375  mapfi  7395  fiin  7419  fiss  7421  oiiso  7498  unwdomg  7544  suc11reg  7566  inf3lem5  7579  infeq5  7584  cantnfp1lem3  7628  r1tr  7694  r1val1  7704  rankr1ai  7716  rankonidlem  7746  onssr1  7749  tskwe  7829  carddom2  7856  carden2  7866  domtri2  7868  cardval2  7870  fidomtri  7872  fidomtri2  7873  harval2  7876  dif1card  7884  infxpenlem  7887  ac5num  7909  alephord3  7951  alephdom  7954  aleph11  7957  alephdom2  7960  cardaleph  7962  dfac3  7994  dfac5  8001  cdacomen  8053  onacda  8069  pwsdompw  8076  ackbij1lem11  8102  ackbij2  8115  cfeq0  8128  cfsuc  8129  cff1  8130  cflim2  8135  cfsmolem  8142  coftr  8145  sornom  8149  infpssrlem4  8178  ssfin4  8182  ssfin2  8192  ssfin3ds  8202  fin23lem31  8215  isf32lem9  8233  hsmexlem5  8302  axdc3lem  8322  axdc3lem2  8323  axdc3lem4  8325  zorn2lem6  8373  brdom3  8398  brdom7disj  8401  brdom6disj  8402  alephval2  8439  alephreg  8449  wuncss  8612  gruen  8679  addcompi  8763  mulcompi  8765  ltapi  8772  ltmpi  8773  nqereu  8798  addcompq  8819  addcomnq  8820  mulcompq  8821  mulcomnq  8822  ltsonq  8838  ltanq  8840  ltmnq  8841  genpnnp  8874  addcompr  8890  mulcompr  8892  ltsopr  8901  ltexprlem2  8906  prlem936  8916  suplem2pr  8922  map2psrpr  8977  axpre-ltadd  9034  xrltnle  9136  axlttri  9139  axsup  9143  ltnle  9147  letri3  9152  leloe  9153  eqlelt  9154  letric  9166  mul31  9226  subcl  9297  pncan2  9304  pncan3  9305  npcan  9306  addsubeq4  9312  npncan3  9331  negsubdi2  9352  muladd  9458  subdi  9459  mulneg2  9463  mulsub  9468  ltleadd  9503  ltsubpos  9512  posdif  9513  addge01  9530  lesub0  9536  wloglei  9551  prodgt02  9848  prodge02  9850  ltdivmul  9874  ledivmul  9875  lt2mul2div  9878  lerec  9884  lt2msq  9886  ltdiv23  9893  lediv23  9894  lediv2a  9896  le2msq  9902  msq11  9903  fimaxre  9947  lbreu  9950  infm3  9959  dfinfmr  9977  creur  9986  creui  9987  cju  9988  nnmulcl  10015  nndivtr  10033  avgle1  10199  avgle2  10200  avgle  10201  nn0nnaddcl  10244  zrevaddcl  10313  znnsub  10314  znn0sub  10315  zextlt  10336  gtndiv  10339  prime  10342  uztrn2  10495  uztric  10499  uz11  10500  uzwo  10531  uzwoOLD  10532  zmax  10563  zbtwnre  10564  rebtwnz  10565  qrevaddcl  10588  rpnnen1lem1  10592  rpnnen1lem2  10593  rpnnen1lem3  10594  rpnnen1lem5  10596  difrp  10637  xrltnsym  10722  xrlttri  10724  xrleloe  10729  xrletri  10736  xrletri3  10737  xrmaxeq  10759  xrmineq  10760  xrmaxlt  10761  xrmaxle  10763  z2ge  10776  qbtwnre  10777  qextlt  10781  qextle  10782  xleneg  10796  xaddcom  10816  xmulcom  10837  xmulneg2  10841  xmulgt0  10854  xrsupsslem  10877  xrinfmsslem  10878  supxrunb1  10890  supxrunb2  10891  ixxssixx  10922  ixxin  10925  ioon0  10934  iccid  10953  iooshf  10981  iccsupr  10989  iooneg  11009  iccneg  11010  iccsplit  11021  fzen  11064  fzass4  11082  fzrev  11100  fznn  11107  elfzm1b  11117  fzm1  11119  fzon  11150  fllt  11207  flbi  11215  flbi2  11216  flzadd  11220  modcyc2  11269  om2uzlt2i  11283  om2uzf1oi  11285  fseqsupubi  11309  expcllem  11384  faclbnd5  11581  hashbnd  11616  hasheni  11624  hasheqf1oi  11627  hashdom  11645  hashfacen  11695  ccatass  11742  ccatco  11796  shftlem  11875  shftuz  11876  shftfval  11877  shftval4  11884  shftval5  11885  2shfti  11887  seqshft  11892  mulre  11918  sqrlt  12059  abs3dif  12127  abs2difabs  12130  uzin2  12140  rexanre  12142  caubnd  12154  climshftlem  12360  rlimcn2  12376  fsumcnv  12549  geo2lim  12644  efle  12711  reef11  12712  demoivre  12793  demoivreALT  12794  sqr2irr  12840  0dvds  12862  muldvds1  12866  muldvds2  12867  dvdscmulr  12870  dvdssubr  12883  dvdsadd2b  12884  odd2np1  12900  divalglem9  12913  ndvdssub  12919  gcdcllem1  13003  gcdcom  13012  neggcd  13019  gcdabs2  13027  modgcd  13028  dvdsprm  13091  coprmdvds  13094  qredeq  13098  odzdvds  13173  coprimeprodsq  13175  pythagtriplem1  13182  pythagtriplem4  13185  pc2dvds  13244  pc11  13245  pcz  13246  pcprod  13256  prmunb  13274  1arithlem3  13285  1arith  13287  ressabs  13519  acsfn2  13880  issect  13971  pospo  14422  clatglbss  14546  pospropd  14553  pslem  14630  tsrss  14647  spweu  14651  issubmnd  14716  submcl  14745  resmhm2b  14753  frmdmnd  14796  frmd0  14797  grpinvsub  14863  gimcnv  15046  gimco  15047  gictr  15054  cntz2ss  15123  cntzrec  15124  dfod2  15192  lsmcom2  15281  efgred  15372  divsabl  15472  cygabl  15492  eldprd  15554  dfrhm2  15813  lmimcnv  16131  psrbagsuppfi  16557  cnfldexp  16726  cnsrng  16727  xrsdsreval  16735  dvdsrz  16759  znf1o  16824  ocvocv  16890  ocvin  16893  eltg  17014  eltg2  17015  tgss  17025  tgss2  17044  basgen2  17046  bastop1  17050  cldmre  17134  toponmre  17149  opnneiss  17174  restcldr  17230  restfpw  17235  restcls  17237  restntr  17238  ordtbaslem  17244  ordtrest2lem  17259  leordtvallem2  17267  leordtval  17269  cnrest  17341  t0sep  17380  cmpcov  17444  cmpsublem  17454  cmpsub  17455  2ndcomap  17513  ptval  17594  xkoval  17611  txss12  17629  ptrescn  17663  xkopt  17679  hmeofval  17782  txswaphmeolem  17828  txswaphmeo  17829  trfbas2  17867  trfbas  17868  uzrest  17921  numufl  17939  ssufl  17942  flimclsi  18002  hauspwpwf1  18011  ghmcnp  18136  blpnfctr  18458  metequiv  18531  metcnp3  18562  elbl4  18598  restmetu  18609  tngngp  18687  qtopbaslem  18784  bl2ioo  18815  ioo2bl  18816  ioo2blex  18817  xrsxmet  18832  divccn  18895  divccncf  18928  causs  19243  lmclim  19247  bcthlem1  19269  ovolfsf  19360  ioombl  19451  iccvolcl  19453  ioorcl  19461  volcn  19490  itg2itg1  19620  dvexp  19831  dvmptfsum  19851  dvexp3  19854  dvef  19856  dvlip  19869  c1lip1  19873  ftc1a  19913  tdeglem1  19973  tdeglem3  19974  tdeglem4  19975  coe1termlem  20168  plyremlem  20213  ptolemy  20396  cos11  20427  logeftb  20470  logleb  20490  logdivlt  20508  logdivle  20509  angval  20635  isppw2  20890  issqf  20911  vmasum  20992  lgsquadlem3  21132  ostth  21325  nb3graprlem2  21453  isspthonpth  21576  wlkdvspthlem  21599  3v3e3cycl1  21623  constr3trllem2  21630  constr3trllem3  21631  eupatrl  21682  ablomul  21935  isdivrngo  22011  vcz  22041  isvc  22052  isnv  22083  isnvi  22084  nmooge0  22260  nmblolbii  22292  blocnilem  22297  ipblnfi  22349  hvpncan2  22534  hvaddsub4  22572  hire  22588  abshicom  22595  hial2eq2  22601  orthcom  22602  hhssabloi  22754  ocsh  22777  shscli  22811  shscom  22813  shsel2  22816  spanss  22842  shjcom  22852  shmodsi  22883  chpsscon3  22997  spansni  23051  spansnmul  23058  spansncol  23062  spanunsni  23073  cmcm2  23110  cm2j  23114  spansncvi  23146  5oalem2  23149  3oalem2  23157  honegsubdi2  23306  adjsym  23328  cnvadj  23387  brafn  23442  kbpj  23451  riesz3i  23557  cnlnadjlem2  23563  cnlnadjlem9  23570  nmopcoi  23590  cnvbraval  23605  leop  23618  leop3  23620  leopmul2i  23630  leoptri  23631  hstrlem3a  23755  cvcon3  23779  cvnsym  23785  mdbr2  23791  dmdmd  23795  dmdbr2  23798  dmdbr3  23800  dmdbr4  23801  dmdbr5  23803  mdsl0  23805  ssmd2  23807  mdslmd1lem1  23820  mdslmd1lem2  23821  mdslmd3i  23827  mdslmd4i  23828  atcveq0  23843  superpos  23849  atnemeq0  23872  atssma  23873  atexch  23876  atomli  23877  atcvatlem  23880  atcvati  23881  chirredlem1  23885  chirredlem3  23887  chirredi  23889  atcvat3i  23891  atdmd  23893  mdsymlem1  23898  mdsymlem3  23900  mdsymlem4  23901  mdsymlem5  23902  mdsymlem8  23905  dmdsym  23908  atdmd2  23909  sumdmdlem  23913  cdjreui  23927  cdj3lem2b  23932  cdj3i  23936  imadifxp  24030  abfmpel  24059  xaddeq0  24111  xrofsup  24118  xeqlelt  24131  xdivpnfrp  24171  xrsinvgval  24191  xrsmulgzz  24192  cnvordtrestixx  24303  indval  24403  esumpfinvallem  24456  sigagenss  24524  brae  24584  dya2iocival  24615  dya2iocnei  24624  dya2iocuni  24625  derangenlem  24849  subfacval2  24865  kur14  24894  elfzp1b  25108  lediv2aALT  25109  mulsuble0b  25185  ntrivcvgfvn0  25219  prodmo  25254  zprod  25255  prodss  25265  fprodcnv  25299  faclim2  25359  funpsstri  25381  setlikespec  25454  dftrpred3g  25503  soseq  25521  wfr3g  25529  wfrlem5  25534  wfrlem10  25539  wsuclem  25568  frrlem5  25578  elno  25593  sltsolem1  25615  nodenselem4  25631  nofulllem5  25653  brbtwn2  25836  colinearalglem4  25840  ax5seglem1  25859  ax5seglem2  25860  axcontlem2  25896  axcontlem12  25906  bpolysum  26091  bpoly4  26097  hfelhf  26114  onsuct0  26183  nndivsub  26199  ltflcei  26231  leceifl  26232  lxflflp1  26233  mblfinlem2  26235  mblfinlem3  26236  ismblfin  26237  ovoliunnfl  26238  voliunnfl  26240  volsupnfl  26241  cnambfre  26245  itg2addnclem2  26247  itg2addnc  26249  itg2gt0cn  26250  ftc1anclem1  26270  ftc1anclem4  26273  ftc1anclem6  26275  ftc1anclem7  26276  ftc1anc  26278  elicc3  26311  nn0prpwlem  26316  nn0prpw  26317  isfne  26339  locfincmp  26375  unirep  26405  opelopab3  26409  fvopabf4g  26413  indexa  26426  filbcmb  26433  fzadd2  26436  incsequz2  26444  metf1o  26452  sstotbnd3  26476  isbnd2  26483  bndss  26486  ismtycnv  26502  iccbnd  26540  exidreslem  26543  exidresid  26545  ghomco  26549  isdrngo2  26565  rngoisocnv  26588  riscer  26595  crngohomfo  26607  unichnidl  26632  maxidlmax  26644  igenmin  26665  prtlem16  26709  ismrc  26746  nacsfg  26750  isnacs3  26755  incssnn0  26756  elmapssres  26762  mzpclall  26775  lerabdioph  26856  ltrabdioph  26859  eldioph4b  26863  jm2.17b  27017  congrep  27029  unxpwdom3  27224  islindf  27250  lindff  27253  lindfrn  27259  f1lindf  27260  lnr2i  27288  pmtrfinv  27370  mamudir  27430  matsca2  27442  matbas2  27443  matlmod  27447  expgrowth  27520  2sbc6g  27583  2sbc5g  27584  ordpss  27621  addrcom  27647  fmul01  27677  ioovolcl  27709  stoweidlem34  27750  sigarac  27809  2reu3  27933  afv0nbfvbi  27982  dmfcoafv  28006  ltnltne  28079  fz0fzdiffz0  28103  ubmelm1fzo  28110  fzonmapblen  28117  ltdifltdiv  28126  modifeq2int  28139  ccatsymb  28152  swrdltnd  28153  swrdccatin12lem3b  28175  swrdccatin2  28176  swrdccatin12lem3  28178  swrdccatin12  28180  swrdccat3blem  28184  cshwidx  28208  cshwidxm  28212  cshwidxn  28213  2cshw1lem1  28214  2cshw1lem3  28216  2cshw2lem1  28218  2cshw2lem2  28219  2cshw2lem3  28220  2cshwmod  28223  lswrdcshw  28229  2cshwcom  28230  cshweqrep  28237  cshwssizelem4a  28246  cshwssizelem4  28247  frgra3v  28329  frgraregorufr  28379  usg2spot2nb  28391  3impcombi  28866  sspwimp  28967  sspwimpVD  28968  a9e2ndeqALT  28980  iunconlem2  28984  sineq0ALT  28986  bnj934  29243  paddss1  30551  paddss2  30552  paddss12  30553  pclfinN  30634  erngmul-rN  31548  mapdordlem2  32372
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator