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  2068  nfeud2  2293  2eu1  2361  2eu3  2363  eqeqan12rd  2452  sylan9eqr  2490  r19.29_2a  2852  morex  3118  sbcrext  3234  sylan9ssr  3362  pssdifcom1  3713  pssdifcom2  3714  riinn0  4165  breqan12rd  4228  ordelssne  4608  ordtri3or  4613  ordtri2  4616  ordtri4  4618  ordtr2  4625  ordtr3  4626  ordintdif  4630  ordtri2or  4677  dfwe2  4762  ordsucelsuc  4802  ordunisuc2  4824  tfindsg  4840  tfindsg2  4841  dfom2  4847  soinxp  4942  frinxp  4943  seinxp  4944  brelrng  5099  dminss  5286  imainss  5287  funsng  5497  funcnvuni  5518  f1co  5648  f1ocnv  5687  fun11iun  5695  f1oprswap  5717  funimass4  5777  dffv2  5796  fndmdifcom  5835  fsn2  5908  fvtp2  5940  fvtp3  5941  fvtp2g  5943  fvtp3g  5944  cofunex2g  5960  soisoi  6048  oveqan12rd  6101  curry2  6441  soxp  6459  mpt2xopoveqd  6472  tposoprab  6515  brrpssg  6524  sorpsscmpl  6533  smores3  6615  smores2  6616  smoel  6622  tfr3  6660  tz7.48-2  6699  tz7.49  6702  oaordi  6789  oaword  6792  oaord1  6794  oaword2  6796  oa00  6802  oalimcl  6803  oaass  6804  oarec  6805  oacomf1o  6808  omord2  6810  omcan  6812  omword  6813  omword1  6816  omword2  6817  odi  6822  omass  6823  oneo  6824  oen0  6829  oecan  6832  oelim2  6838  nnarcl  6859  nnaordi  6861  nnaordr  6863  nnawordi  6864  nnmsucr  6868  nnmcom  6869  nnaword  6870  nnmordi  6874  nnaordex  6881  oaabslem  6886  omabslem  6889  nnneo  6894  omsmo  6897  ersym  6917  elecg  6943  riiner  6977  ecopovsym  7006  ecovcom  7015  mapvalg  7028  pmvalg  7029  elpmg  7032  pmss12g  7040  ixpconstg  7071  ener  7154  domtr  7160  f1imaeng  7167  fundmen  7180  xpcomco  7198  xpsnen2g  7201  xpdom2  7203  xpdom1g  7205  omxpen  7210  omf1o  7211  enen2  7248  domen2  7250  sdomen2  7252  domtriord  7253  sdomel  7254  onsdominel  7256  infensuc  7285  onomeneq  7296  nndomo  7300  pssnn  7327  unbnn  7363  infcntss  7380  fiint  7383  mapfi  7403  fiin  7427  fiss  7429  oiiso  7506  unwdomg  7552  suc11reg  7574  inf3lem5  7587  infeq5  7592  cantnfp1lem3  7636  r1tr  7702  r1val1  7712  rankr1ai  7724  rankonidlem  7754  onssr1  7757  tskwe  7837  carddom2  7864  carden2  7874  domtri2  7876  cardval2  7878  fidomtri  7880  fidomtri2  7881  harval2  7884  dif1card  7892  infxpenlem  7895  ac5num  7917  alephord3  7959  alephdom  7962  aleph11  7965  alephdom2  7968  cardaleph  7970  dfac3  8002  dfac5  8009  cdacomen  8061  onacda  8077  pwsdompw  8084  ackbij1lem11  8110  ackbij2  8123  cfeq0  8136  cfsuc  8137  cff1  8138  cflim2  8143  cfsmolem  8150  coftr  8153  sornom  8157  infpssrlem4  8186  ssfin4  8190  ssfin2  8200  ssfin3ds  8210  fin23lem31  8223  isf32lem9  8241  hsmexlem5  8310  axdc3lem  8330  axdc3lem2  8331  axdc3lem4  8333  zorn2lem6  8381  brdom3  8406  brdom7disj  8409  brdom6disj  8410  alephval2  8447  alephreg  8457  wuncss  8620  gruen  8687  addcompi  8771  mulcompi  8773  ltapi  8780  ltmpi  8781  nqereu  8806  addcompq  8827  addcomnq  8828  mulcompq  8829  mulcomnq  8830  ltsonq  8846  ltanq  8848  ltmnq  8849  genpnnp  8882  addcompr  8898  mulcompr  8900  ltsopr  8909  ltexprlem2  8914  prlem936  8924  suplem2pr  8930  map2psrpr  8985  axpre-ltadd  9042  xrltnle  9144  axlttri  9147  axsup  9151  ltnle  9155  letri3  9160  leloe  9161  eqlelt  9162  letric  9174  mul31  9234  subcl  9305  pncan2  9312  pncan3  9313  npcan  9314  addsubeq4  9320  npncan3  9339  negsubdi2  9360  muladd  9466  subdi  9467  mulneg2  9471  mulsub  9476  ltleadd  9511  ltsubpos  9520  posdif  9521  addge01  9538  lesub0  9544  wloglei  9559  prodgt02  9856  prodge02  9858  ltdivmul  9882  ledivmul  9883  lt2mul2div  9886  lerec  9892  lt2msq  9894  ltdiv23  9901  lediv23  9902  lediv2a  9904  le2msq  9910  msq11  9911  fimaxre  9955  lbreu  9958  infm3  9967  dfinfmr  9985  creur  9994  creui  9995  cju  9996  nnmulcl  10023  nndivtr  10041  avgle1  10207  avgle2  10208  avgle  10209  nn0nnaddcl  10252  zrevaddcl  10321  znnsub  10322  znn0sub  10323  zextlt  10344  gtndiv  10347  prime  10350  uztrn2  10503  uztric  10507  uz11  10508  uzwo  10539  uzwoOLD  10540  zmax  10571  zbtwnre  10572  rebtwnz  10573  qrevaddcl  10596  rpnnen1lem1  10600  rpnnen1lem2  10601  rpnnen1lem3  10602  rpnnen1lem5  10604  difrp  10645  xrltnsym  10730  xrlttri  10732  xrleloe  10737  xrletri  10744  xrletri3  10745  xrmaxeq  10767  xrmineq  10768  xrmaxlt  10769  xrmaxle  10771  z2ge  10784  qbtwnre  10785  qextlt  10789  qextle  10790  xleneg  10804  xaddcom  10824  xmulcom  10845  xmulneg2  10849  xmulgt0  10862  xrsupsslem  10885  xrinfmsslem  10886  supxrunb1  10898  supxrunb2  10899  ixxssixx  10930  ixxin  10933  ioon0  10942  iccid  10961  iooshf  10989  iccsupr  10997  iooneg  11017  iccneg  11018  iccsplit  11029  fzen  11072  fzass4  11090  fzrev  11108  fznn  11115  elfzm1b  11125  fzm1  11127  fzon  11158  fllt  11215  flbi  11223  flbi2  11224  flzadd  11228  modcyc2  11277  om2uzlt2i  11291  om2uzf1oi  11293  fseqsupubi  11317  expcllem  11392  faclbnd5  11589  hashbnd  11624  hasheni  11632  hasheqf1oi  11635  hashdom  11653  hashfacen  11703  ccatass  11750  ccatco  11804  shftlem  11883  shftuz  11884  shftfval  11885  shftval4  11892  shftval5  11893  2shfti  11895  seqshft  11900  mulre  11926  sqrlt  12067  abs3dif  12135  abs2difabs  12138  uzin2  12148  rexanre  12150  caubnd  12162  climshftlem  12368  rlimcn2  12384  fsumcnv  12557  geo2lim  12652  efle  12719  reef11  12720  demoivre  12801  demoivreALT  12802  sqr2irr  12848  0dvds  12870  muldvds1  12874  muldvds2  12875  dvdscmulr  12878  dvdssubr  12891  dvdsadd2b  12892  odd2np1  12908  divalglem9  12921  ndvdssub  12927  gcdcllem1  13011  gcdcom  13020  neggcd  13027  gcdabs2  13035  modgcd  13036  dvdsprm  13099  coprmdvds  13102  qredeq  13106  odzdvds  13181  coprimeprodsq  13183  pythagtriplem1  13190  pythagtriplem4  13193  pc2dvds  13252  pc11  13253  pcz  13254  pcprod  13264  prmunb  13282  1arithlem3  13293  1arith  13295  ressabs  13527  acsfn2  13888  issect  13979  pospo  14430  clatglbss  14554  pospropd  14561  pslem  14638  tsrss  14655  spweu  14659  issubmnd  14724  submcl  14753  resmhm2b  14761  frmdmnd  14804  frmd0  14805  grpinvsub  14871  gimcnv  15054  gimco  15055  gictr  15062  cntz2ss  15131  cntzrec  15132  dfod2  15200  lsmcom2  15289  efgred  15380  divsabl  15480  cygabl  15500  eldprd  15562  dfrhm2  15821  lmimcnv  16139  psrbagsuppfi  16565  cnfldexp  16734  cnsrng  16735  xrsdsreval  16743  dvdsrz  16767  znf1o  16832  ocvocv  16898  ocvin  16901  eltg  17022  eltg2  17023  tgss  17033  tgss2  17052  basgen2  17054  bastop1  17058  cldmre  17142  toponmre  17157  opnneiss  17182  restcldr  17238  restfpw  17243  restcls  17245  restntr  17246  ordtbaslem  17252  ordtrest2lem  17267  leordtvallem2  17275  leordtval  17277  cnrest  17349  t0sep  17388  cmpcov  17452  cmpsublem  17462  cmpsub  17463  2ndcomap  17521  ptval  17602  xkoval  17619  txss12  17637  ptrescn  17671  xkopt  17687  hmeofval  17790  txswaphmeolem  17836  txswaphmeo  17837  trfbas2  17875  trfbas  17876  uzrest  17929  numufl  17947  ssufl  17950  flimclsi  18010  hauspwpwf1  18019  ghmcnp  18144  blpnfctr  18466  metequiv  18539  metcnp3  18570  elbl4  18606  restmetu  18617  tngngp  18695  qtopbaslem  18792  bl2ioo  18823  ioo2bl  18824  ioo2blex  18825  xrsxmet  18840  divccn  18903  divccncf  18936  causs  19251  lmclim  19255  bcthlem1  19277  ovolfsf  19368  ioombl  19459  iccvolcl  19461  ioorcl  19469  volcn  19498  itg2itg1  19628  dvexp  19839  dvmptfsum  19859  dvexp3  19862  dvef  19864  dvlip  19877  c1lip1  19881  ftc1a  19921  tdeglem1  19981  tdeglem3  19982  tdeglem4  19983  coe1termlem  20176  plyremlem  20221  ptolemy  20404  cos11  20435  logeftb  20478  logleb  20498  logdivlt  20516  logdivle  20517  angval  20643  isppw2  20898  issqf  20919  vmasum  21000  lgsquadlem3  21140  ostth  21333  nb3graprlem2  21461  isspthonpth  21584  wlkdvspthlem  21607  3v3e3cycl1  21631  constr3trllem2  21638  constr3trllem3  21639  eupatrl  21690  ablomul  21943  isdivrngo  22019  vcz  22049  isvc  22060  isnv  22091  isnvi  22092  nmooge0  22268  nmblolbii  22300  blocnilem  22305  ipblnfi  22357  hvpncan2  22542  hvaddsub4  22580  hire  22596  abshicom  22603  hial2eq2  22609  orthcom  22610  hhssabloi  22762  ocsh  22785  shscli  22819  shscom  22821  shsel2  22824  spanss  22850  shjcom  22860  shmodsi  22891  chpsscon3  23005  spansni  23059  spansnmul  23066  spansncol  23070  spanunsni  23081  cmcm2  23118  cm2j  23122  spansncvi  23154  5oalem2  23157  3oalem2  23165  honegsubdi2  23314  adjsym  23336  cnvadj  23395  brafn  23450  kbpj  23459  riesz3i  23565  cnlnadjlem2  23571  cnlnadjlem9  23578  nmopcoi  23598  cnvbraval  23613  leop  23626  leop3  23628  leopmul2i  23638  leoptri  23639  hstrlem3a  23763  cvcon3  23787  cvnsym  23793  mdbr2  23799  dmdmd  23803  dmdbr2  23806  dmdbr3  23808  dmdbr4  23809  dmdbr5  23811  mdsl0  23813  ssmd2  23815  mdslmd1lem1  23828  mdslmd1lem2  23829  mdslmd3i  23835  mdslmd4i  23836  atcveq0  23851  superpos  23857  atnemeq0  23880  atssma  23881  atexch  23884  atomli  23885  atcvatlem  23888  atcvati  23889  chirredlem1  23893  chirredlem3  23895  chirredi  23897  atcvat3i  23899  atdmd  23901  mdsymlem1  23906  mdsymlem3  23908  mdsymlem4  23909  mdsymlem5  23910  mdsymlem8  23913  dmdsym  23916  atdmd2  23917  sumdmdlem  23921  cdjreui  23935  cdj3lem2b  23940  cdj3i  23944  imadifxp  24038  abfmpel  24067  xaddeq0  24119  xrofsup  24126  xeqlelt  24139  xdivpnfrp  24179  xrsinvgval  24199  xrsmulgzz  24200  cnvordtrestixx  24311  indval  24411  esumpfinvallem  24464  sigagenss  24532  brae  24592  dya2iocival  24623  dya2iocnei  24632  dya2iocuni  24633  derangenlem  24857  subfacval2  24873  kur14  24902  elfzp1b  25116  lediv2aALT  25117  mulsuble0b  25193  ntrivcvgfvn0  25227  prodmo  25262  zprod  25263  prodss  25273  fprodcnv  25307  faclim2  25367  funpsstri  25389  setlikespec  25462  dftrpred3g  25511  soseq  25529  wfr3g  25537  wfrlem5  25542  wfrlem10  25547  wsuclem  25576  frrlem5  25586  elno  25601  sltsolem1  25623  nodenselem4  25639  nofulllem5  25661  brbtwn2  25844  colinearalglem4  25848  ax5seglem1  25867  ax5seglem2  25868  axcontlem2  25904  axcontlem12  25914  bpolysum  26099  bpoly4  26105  hfelhf  26122  onsuct0  26191  nndivsub  26207  ltflcei  26239  leceifl  26240  lxflflp1  26241  mblfinlem3  26245  mblfinlem4  26246  ismblfin  26247  ovoliunnfl  26248  voliunnfl  26250  volsupnfl  26251  cnambfre  26255  itg2addnclem2  26257  itg2addnc  26259  itg2gt0cn  26260  ftc1anclem1  26280  ftc1anclem4  26283  ftc1anclem6  26285  ftc1anclem7  26286  ftc1anc  26288  elicc3  26320  nn0prpwlem  26325  nn0prpw  26326  isfne  26348  locfincmp  26384  unirep  26414  opelopab3  26418  fvopabf4g  26422  indexa  26435  filbcmb  26442  fzadd2  26445  incsequz2  26453  metf1o  26461  sstotbnd3  26485  isbnd2  26492  bndss  26495  ismtycnv  26511  iccbnd  26549  exidreslem  26552  exidresid  26554  ghomco  26558  isdrngo2  26574  rngoisocnv  26597  riscer  26604  crngohomfo  26616  unichnidl  26641  maxidlmax  26653  igenmin  26674  prtlem16  26718  ismrc  26755  nacsfg  26759  isnacs3  26764  incssnn0  26765  elmapssres  26771  mzpclall  26784  lerabdioph  26865  ltrabdioph  26868  eldioph4b  26872  jm2.17b  27026  congrep  27038  unxpwdom3  27233  islindf  27259  lindff  27262  lindfrn  27268  f1lindf  27269  lnr2i  27297  pmtrfinv  27379  mamudir  27439  matsca2  27451  matbas2  27452  matlmod  27456  expgrowth  27529  2sbc6g  27592  2sbc5g  27593  ordpss  27630  addrcom  27656  fmul01  27686  ioovolcl  27718  stoweidlem34  27759  sigarac  27818  2reu3  27942  afv0nbfvbi  27991  dmfcoafv  28015  ltnltne  28094  fz0fzdiffz0  28119  ubmelm1fzo  28127  fzonmapblen  28134  fzoopth  28139  ltdifltdiv  28148  modifeq2int  28161  ccatsymb  28179  swrdltnd  28181  swrdccatin12lem3b  28209  swrdccatin2  28210  swrdccatin12lem3  28212  swrdccatin12  28214  swrdccat3blem  28218  cshwidx  28242  cshwidxm  28246  cshwidxn  28247  2cshw1lem1  28248  2cshw1lem3  28250  2cshw2lem1  28252  2cshw2lem2  28253  2cshw2lem3  28254  2cshwmod  28257  lswrdcshw  28266  2cshwcom  28267  cshweqrep  28274  cshwssizelem4a  28283  cshwssizelem4  28284  frgra3v  28392  frgraregorufr  28442  usg2spot2nb  28454  3impcombi  28929  sspwimp  29030  sspwimpVD  29031  a9e2ndeqALT  29043  iunconlem2  29047  sineq0ALT  29049  bnj934  29306  paddss1  30614  paddss2  30615  paddss12  30616  pclfinN  30697  erngmul-rN  31611  mapdordlem2  32435
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