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

Theorem ancoms 439
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 424 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32imp 418 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  adantl  452  syl2anr  464  anim12ci  550  sylan9bbr  681  anabss4  788  anabsi7  792  anabsi8  793  im2anan9r  809  bi2anan9r  844  syl3anr2  1235  mp3anr1  1274  mp3anr2  1275  mp3anr3  1276  19.29r  1586  nfeud2  2157  2eu1  2225  2eu3  2227  eqeqan12rd  2301  sylan9eqr  2339  morex  2951  sbcrext  3066  sylan9ssr  3195  pssdifcom1  3541  pssdifcom2  3542  riinn0  3978  breqan12rd  4041  ordelssne  4421  ordtri3or  4426  ordtri2  4429  ordtri4  4431  ordtr2  4438  ordtr3  4439  ordintdif  4443  ordtri2or  4490  dfwe2  4575  ordsucelsuc  4615  ordunisuc2  4637  tfindsg  4653  tfindsg2  4654  dfom2  4660  soinxp  4756  frinxp  4757  seinxp  4758  brelrng  4910  dminss  5097  imainss  5098  funsng  5300  funcnvuni  5319  f1co  5448  f1ocnv  5487  fun11iun  5495  f1oprswap  5517  funimass4  5575  dffv2  5594  fndmdifcom  5632  fsn2  5700  fvtp2  5727  fvtp3  5728  cofunex2g  5742  soisoi  5827  oveqan12rd  5880  curry2  6215  soxp  6230  tposoprab  6272  brrpssg  6281  sorpsscmpl  6290  smores3  6372  smores2  6373  smoel  6379  tfr3  6417  tz7.48-2  6456  tz7.49  6459  oaordi  6546  oaword  6549  oaord1  6551  oaword2  6553  oa00  6559  oalimcl  6560  oaass  6561  oarec  6562  oacomf1o  6565  omord2  6567  omcan  6569  omword  6570  omword1  6573  omword2  6574  odi  6579  omass  6580  oneo  6581  oen0  6586  oecan  6589  oelim2  6595  nnarcl  6616  nnaordi  6618  nnaordr  6620  nnawordi  6621  nnmsucr  6625  nnmcom  6626  nnaword  6627  nnmordi  6631  nnaordex  6638  oaabslem  6643  omabslem  6646  nnneo  6651  omsmo  6654  ersym  6674  elecg  6700  riiner  6734  ecopovsym  6762  ecovcom  6771  mapvalg  6784  pmvalg  6785  elpmg  6788  pmss12g  6796  ixpconstg  6827  ener  6910  domtr  6916  f1imaeng  6923  fundmen  6936  xpcomco  6954  xpsnen2g  6957  xpdom2  6959  xpdom1g  6961  omxpen  6966  omf1o  6967  enen2  7004  domen2  7006  sdomen2  7008  domtriord  7009  sdomel  7010  onsdominel  7012  infensuc  7041  onomeneq  7052  nndomo  7056  pssnn  7083  unbnn  7115  infcntss  7132  fiint  7135  mapfi  7154  fiin  7177  fiss  7179  oiiso  7254  unwdomg  7300  suc11reg  7322  inf3lem5  7335  infeq5  7340  cantnfp1lem3  7384  r1tr  7450  r1val1  7460  rankr1ai  7472  rankonidlem  7502  onssr1  7505  tskwe  7585  carddom2  7612  carden2  7622  domtri2  7624  cardval2  7626  fidomtri  7628  fidomtri2  7629  harval2  7632  dif1card  7640  infxpenlem  7643  ac5num  7665  alephord3  7707  alephdom  7710  aleph11  7713  alephdom2  7716  cardaleph  7718  dfac3  7750  dfac5  7757  cdacomen  7809  onacda  7825  pwsdompw  7832  ackbij1lem11  7858  ackbij2  7871  cfeq0  7884  cfsuc  7885  cff1  7886  cflim2  7891  cfsmolem  7898  coftr  7901  sornom  7905  infpssrlem4  7934  ssfin4  7938  ssfin2  7948  ssfin3ds  7958  fin23lem31  7971  isf32lem9  7989  hsmexlem5  8058  axdc3lem  8078  axdc3lem2  8079  axdc3lem4  8081  zorn2lem6  8130  brdom3  8155  brdom7disj  8158  brdom6disj  8159  alephval2  8196  alephreg  8206  wuncss  8369  gruen  8436  addcompi  8520  mulcompi  8522  ltapi  8529  ltmpi  8530  nqereu  8555  addcompq  8576  addcomnq  8577  mulcompq  8578  mulcomnq  8579  ltsonq  8595  ltanq  8597  ltmnq  8598  genpnnp  8631  addcompr  8647  mulcompr  8649  ltsopr  8658  ltexprlem2  8663  prlem936  8673  suplem2pr  8679  map2psrpr  8734  axpre-ltadd  8791  xrltnle  8893  axlttri  8896  axsup  8900  ltnle  8904  letri3  8909  leloe  8910  eqlelt  8911  letric  8923  mul31  8982  subcl  9053  pncan2  9060  pncan3  9061  npcan  9062  addsubeq4  9068  npncan3  9087  negsubdi2  9108  muladd  9214  subdi  9215  mulneg2  9219  mulsub  9224  ltleadd  9259  ltsubpos  9268  posdif  9269  addge01  9286  lesub0  9292  wloglei  9307  prodgt02  9604  prodge02  9606  ltdivmul  9630  ledivmul  9631  lt2mul2div  9634  lerec  9640  lt2msq  9642  ltdiv23  9649  lediv23  9650  lediv2a  9652  le2msq  9658  msq11  9659  fimaxre  9703  lbreu  9706  infm3  9715  dfinfmr  9733  creur  9742  creui  9743  cju  9744  nnmulcl  9771  nndivtr  9789  avgle1  9953  avgle2  9954  avgle  9955  nn0nnaddcl  9998  zrevaddcl  10065  znnsub  10066  znn0sub  10067  zextlt  10088  gtndiv  10091  prime  10094  uztrn2  10247  uztric  10251  uz11  10252  uzwo  10283  uzwoOLD  10284  zmax  10315  zbtwnre  10316  rebtwnz  10317  qrevaddcl  10340  rpnnen1lem1  10344  rpnnen1lem2  10345  rpnnen1lem3  10346  rpnnen1lem5  10348  difrp  10389  xrltnsym  10473  xrlttri  10475  xrleloe  10480  xrletri  10487  xrletri3  10488  xrmaxeq  10510  xrmineq  10511  xrmaxlt  10512  xrmaxle  10514  z2ge  10527  qbtwnre  10528  qextlt  10532  qextle  10533  xleneg  10547  xaddcom  10567  xmulcom  10588  xmulneg2  10592  xmulgt0  10605  xrsupsslem  10627  xrinfmsslem  10628  supxrunb1  10640  supxrunb2  10641  ixxssixx  10672  ixxin  10675  ioon0  10684  iccid  10703  iooshf  10730  iccsupr  10738  iooneg  10758  iccneg  10759  iccsplit  10770  fzen  10813  fzass4  10831  fzrev  10848  fznn  10854  elfzm1b  10862  fzm1  10864  fllt  10940  flbi  10948  flbi2  10949  flzadd  10953  modcyc2  11002  om2uzlt2i  11016  om2uzf1oi  11018  fseqsupubi  11042  expcllem  11116  faclbnd5  11313  hashbnd  11345  hasheni  11349  hashdom  11363  hashfacen  11394  ccatass  11438  ccatco  11492  shftlem  11565  shftuz  11566  shftfval  11567  shftval4  11574  shftval5  11575  2shfti  11577  seqshft  11582  mulre  11608  sqrlt  11749  abs3dif  11817  abs2difabs  11820  uzin2  11830  rexanre  11832  caubnd  11844  climshftlem  12050  rlimcn2  12066  fsumcnv  12238  geo2lim  12333  efle  12400  reef11  12401  demoivre  12482  demoivreALT  12483  sqr2irr  12529  0dvds  12551  muldvds1  12555  muldvds2  12556  dvdscmulr  12559  dvdssubr  12572  dvdsadd2b  12573  odd2np1  12589  divalglem9  12602  ndvdssub  12608  gcdcllem1  12692  gcdcom  12701  neggcd  12708  gcdabs2  12716  modgcd  12717  dvdsprm  12780  coprmdvds  12783  qredeq  12787  odzdvds  12862  coprimeprodsq  12864  pythagtriplem1  12871  pythagtriplem4  12874  pc2dvds  12933  pc11  12934  pcz  12935  pcprod  12945  prmunb  12963  1arithlem3  12974  1arith  12976  ressabs  13208  acsfn2  13567  issect  13658  pospo  14109  clatglbss  14233  pospropd  14240  pslem  14317  tsrss  14334  spweu  14338  issubmnd  14403  submcl  14432  resmhm2b  14440  frmdmnd  14483  frmd0  14484  grpinvsub  14550  gimcnv  14733  gimco  14734  gictr  14741  cntz2ss  14810  cntzrec  14811  dfod2  14879  lsmcom2  14968  efgred  15059  divsabl  15159  cygabl  15179  eldprd  15241  dfrhm2  15500  lmimcnv  15822  psrbagsuppfi  16248  cnfldexp  16409  cnsrng  16410  xrsdsreval  16418  dvdsrz  16442  znf1o  16507  ocvocv  16573  ocvin  16576  eltg  16697  eltg2  16698  tgss  16708  tgss2  16727  basgen2  16729  bastop1  16733  cldmre  16817  toponmre  16832  opnneiss  16857  restcldr  16907  restfpw  16912  restcls  16913  restntr  16914  ordtbaslem  16920  ordtrest2lem  16935  leordtvallem2  16943  leordtval  16945  cnrest  17015  t0sep  17054  cmpcov  17118  cmpsublem  17128  cmpsub  17129  2ndcomap  17186  ptval  17267  xkoval  17284  txss12  17302  ptrescn  17335  xkopt  17351  hmeofval  17451  txswaphmeolem  17497  txswaphmeo  17498  trfbas2  17540  trfbas  17541  uzrest  17594  numufl  17612  ssufl  17615  flimclsi  17675  hauspwpwf1  17684  ghmcnp  17799  blpnfctr  17984  metequiv  18057  metcnp3  18088  tngngp  18172  qtopbaslem  18269  bl2ioo  18300  ioo2bl  18301  ioo2blex  18302  xrsxmet  18317  divccn  18379  divccncf  18412  causs  18726  lmclim  18730  bcthlem1  18748  ovolfsf  18833  ioombl  18924  iccvolcl  18926  ioorcl  18934  volcn  18963  itg2itg1  19093  dvexp  19304  dvmptfsum  19324  dvexp3  19327  dvef  19329  dvlip  19342  c1lip1  19346  ftc1a  19386  tdeglem1  19446  tdeglem3  19447  tdeglem4  19448  coe1termlem  19641  plyremlem  19686  ptolemy  19866  cos11  19897  logeftb  19939  logleb  19959  logdivlt  19974  logdivle  19975  angval  20101  isppw2  20355  issqf  20376  vmasum  20457  lgsquadlem3  20597  ostth  20790  ablomul  21024  isdivrngo  21100  vcz  21128  isvc  21139  isnv  21170  isnvi  21171  nmooge0  21347  nmblolbii  21379  blocnilem  21384  ipblnfi  21436  hvpncan2  21621  hvaddsub4  21659  hire  21675  abshicom  21682  hial2eq2  21688  orthcom  21689  hhssabloi  21841  ocsh  21864  shscli  21898  shscom  21900  shsel2  21903  spanss  21929  shjcom  21939  shmodsi  21970  chpsscon3  22084  spansni  22138  spansnmul  22145  spansncol  22149  spanunsni  22160  cmcm2  22197  cm2j  22201  spansncvi  22233  5oalem2  22236  3oalem2  22244  honegsubdi2  22393  adjsym  22415  cnvadj  22474  brafn  22529  kbpj  22538  riesz3i  22644  cnlnadjlem2  22650  cnlnadjlem9  22657  nmopcoi  22677  cnvbraval  22692  leop  22705  leop3  22707  leopmul2i  22717  leoptri  22718  hstrlem3a  22842  cvcon3  22866  cvnsym  22872  mdbr2  22878  dmdmd  22882  dmdbr2  22885  dmdbr3  22887  dmdbr4  22888  dmdbr5  22890  mdsl0  22892  ssmd2  22894  mdslmd1lem1  22907  mdslmd1lem2  22908  mdslmd3i  22914  mdslmd4i  22915  atcveq0  22930  superpos  22936  atnemeq0  22959  atssma  22960  atexch  22963  atomli  22964  atcvatlem  22967  atcvati  22968  chirredlem1  22972  chirredlem3  22974  chirredi  22976  atcvat3i  22978  atdmd  22980  mdsymlem1  22985  mdsymlem3  22987  mdsymlem4  22988  mdsymlem5  22989  mdsymlem8  22992  dmdsym  22995  atdmd2  22996  sumdmdlem  23000  cdjreui  23014  cdj3lem2b  23019  cdj3i  23023  xdivpnfrp  23119  abfmpel  23221  xrofsup  23257  xeqlelt  23271  cnvordtrestixx  23299  xaddeq0  23306  esumpfinvallem  23444  sigaclci  23495  sigagenss  23512  dya2iocival  23578  indval  23599  derangenlem  23704  subfacval2  23720  kur14  23749  elfzp1b  24014  lediv2aALT  24015  mulsuble0b  24090  funpsstri  24123  setlikespec  24189  dftrpred3g  24238  soseq  24256  wfr3g  24257  wfrlem5  24262  wfrlem10  24267  frrlem5  24287  elno  24302  sltsolem1  24324  nodenselem4  24340  nofulllem5  24362  brbtwn2  24535  colinearalglem4  24539  ax5seglem1  24558  ax5seglem2  24559  axcontlem2  24595  axcontlem12  24605  bpolysum  24790  bpoly4  24796  hfelhf  24813  onsuct0  24882  nndivsub  24898  ltflcei  24930  leceifl  24931  lxflflp1  24932  itg2addnclem2  24934  mappow  25100  celsor  25122  ffvelrnb  25142  mapex2  25151  injsurinj  25160  ubpar  25272  ranncnt  25294  tolat  25297  nelioo5  25522  hmeogrpi  25547  intopcoaconlem3b  25549  cnfilca  25567  limptlimpr2lem1  25585  islimrs3  25592  msr4  25617  mslb1  25618  iintlem1  25621  trdom  25624  cnvtr  25627  lvsovso  25637  supexr  25642  claddrvr  25659  cnegvex2  25671  rnegvex2  25672  intvconlem1  25714  1ded  25749  tartarmap  25899  cardtar  25915  fnctartar3  25920  setiscat  25990  indcls2  26007  clscnc  26021  bsstrs  26157  elicc3  26239  nn0prpwlem  26249  nn0prpw  26250  isfne  26279  locfincmp  26315  unirep  26360  opelopab3  26384  fvopabf4g  26397  indexa  26423  filbcmb  26443  fzadd2  26455  incsequz2  26470  lpss2  26479  metf1o  26480  sstotbnd3  26511  isbnd2  26518  bndss  26521  ismtycnv  26537  iccbnd  26575  exidreslem  26578  exidresid  26580  ghomco  26584  isdrngo2  26600  rngoisocnv  26623  riscer  26630  crngohomfo  26642  unichnidl  26667  maxidlmax  26679  igenmin  26700  prtlem16  26748  ismrc  26787  nacsfg  26791  isnacs3  26796  incssnn0  26797  elmapssres  26803  mzpclall  26816  lerabdioph  26897  ltrabdioph  26900  eldioph4b  26905  jm2.17b  27059  congrep  27071  unxpwdom3  27267  islindf  27293  lindff  27296  lindfrn  27302  f1lindf  27303  lnr2i  27331  pmtrfinv  27413  mamudir  27473  matsca2  27485  matbas2  27486  matlmod  27490  expgrowth  27563  2sbc6g  27626  2sbc5g  27627  ordpss  27665  addrcom  27691  fmul01  27721  ioovolcl  27753  stoweidlem34  27794  sigarac  27853  2reu3  27977  afv0nbfvbi  28025  dmfcoafv  28047  mpt2xopoveqd  28098  frgra3v  28191  biimpa21  28391  3impcombi  28663  sspwimp  28767  sspwimpVD  28768  a9e2ndeqALT  28781  bnj934  29040  paddss1  30079  paddss2  30080  paddss12  30081  pclfinN  30162  erngmul-rN  31076  mapdordlem2  31900
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 177  df-an 360
  Copyright terms: Public domain W3C validator