MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancoms 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  1604  nfeud2  2266  2eu1  2334  2eu3  2336  eqeqan12rd  2420  sylan9eqr  2458  r19.29_2a  2812  morex  3078  sbcrext  3194  sylan9ssr  3322  pssdifcom1  3673  pssdifcom2  3674  riinn0  4125  breqan12rd  4188  ordelssne  4568  ordtri3or  4573  ordtri2  4576  ordtri4  4578  ordtr2  4585  ordtr3  4586  ordintdif  4590  ordtri2or  4636  dfwe2  4721  ordsucelsuc  4761  ordunisuc2  4783  tfindsg  4799  tfindsg2  4800  dfom2  4806  soinxp  4901  frinxp  4902  seinxp  4903  brelrng  5058  dminss  5245  imainss  5246  funsng  5456  funcnvuni  5477  f1co  5607  f1ocnv  5646  fun11iun  5654  f1oprswap  5676  funimass4  5736  dffv2  5755  fndmdifcom  5794  fsn2  5867  fvtp2  5899  fvtp3  5900  fvtp2g  5902  fvtp3g  5903  cofunex2g  5919  soisoi  6007  oveqan12rd  6060  curry2  6400  soxp  6418  mpt2xopoveqd  6431  tposoprab  6474  brrpssg  6483  sorpsscmpl  6492  smores3  6574  smores2  6575  smoel  6581  tfr3  6619  tz7.48-2  6658  tz7.49  6661  oaordi  6748  oaword  6751  oaord1  6753  oaword2  6755  oa00  6761  oalimcl  6762  oaass  6763  oarec  6764  oacomf1o  6767  omord2  6769  omcan  6771  omword  6772  omword1  6775  omword2  6776  odi  6781  omass  6782  oneo  6783  oen0  6788  oecan  6791  oelim2  6797  nnarcl  6818  nnaordi  6820  nnaordr  6822  nnawordi  6823  nnmsucr  6827  nnmcom  6828  nnaword  6829  nnmordi  6833  nnaordex  6840  oaabslem  6845  omabslem  6848  nnneo  6853  omsmo  6856  ersym  6876  elecg  6902  riiner  6936  ecopovsym  6965  ecovcom  6974  mapvalg  6987  pmvalg  6988  elpmg  6991  pmss12g  6999  ixpconstg  7030  ener  7113  domtr  7119  f1imaeng  7126  fundmen  7139  xpcomco  7157  xpsnen2g  7160  xpdom2  7162  xpdom1g  7164  omxpen  7169  omf1o  7170  enen2  7207  domen2  7209  sdomen2  7211  domtriord  7212  sdomel  7213  onsdominel  7215  infensuc  7244  onomeneq  7255  nndomo  7259  pssnn  7286  unbnn  7322  infcntss  7339  fiint  7342  mapfi  7361  fiin  7385  fiss  7387  oiiso  7462  unwdomg  7508  suc11reg  7530  inf3lem5  7543  infeq5  7548  cantnfp1lem3  7592  r1tr  7658  r1val1  7668  rankr1ai  7680  rankonidlem  7710  onssr1  7713  tskwe  7793  carddom2  7820  carden2  7830  domtri2  7832  cardval2  7834  fidomtri  7836  fidomtri2  7837  harval2  7840  dif1card  7848  infxpenlem  7851  ac5num  7873  alephord3  7915  alephdom  7918  aleph11  7921  alephdom2  7924  cardaleph  7926  dfac3  7958  dfac5  7965  cdacomen  8017  onacda  8033  pwsdompw  8040  ackbij1lem11  8066  ackbij2  8079  cfeq0  8092  cfsuc  8093  cff1  8094  cflim2  8099  cfsmolem  8106  coftr  8109  sornom  8113  infpssrlem4  8142  ssfin4  8146  ssfin2  8156  ssfin3ds  8166  fin23lem31  8179  isf32lem9  8197  hsmexlem5  8266  axdc3lem  8286  axdc3lem2  8287  axdc3lem4  8289  zorn2lem6  8337  brdom3  8362  brdom7disj  8365  brdom6disj  8366  alephval2  8403  alephreg  8413  wuncss  8576  gruen  8643  addcompi  8727  mulcompi  8729  ltapi  8736  ltmpi  8737  nqereu  8762  addcompq  8783  addcomnq  8784  mulcompq  8785  mulcomnq  8786  ltsonq  8802  ltanq  8804  ltmnq  8805  genpnnp  8838  addcompr  8854  mulcompr  8856  ltsopr  8865  ltexprlem2  8870  prlem936  8880  suplem2pr  8886  map2psrpr  8941  axpre-ltadd  8998  xrltnle  9100  axlttri  9103  axsup  9107  ltnle  9111  letri3  9116  leloe  9117  eqlelt  9118  letric  9130  mul31  9190  subcl  9261  pncan2  9268  pncan3  9269  npcan  9270  addsubeq4  9276  npncan3  9295  negsubdi2  9316  muladd  9422  subdi  9423  mulneg2  9427  mulsub  9432  ltleadd  9467  ltsubpos  9476  posdif  9477  addge01  9494  lesub0  9500  wloglei  9515  prodgt02  9812  prodge02  9814  ltdivmul  9838  ledivmul  9839  lt2mul2div  9842  lerec  9848  lt2msq  9850  ltdiv23  9857  lediv23  9858  lediv2a  9860  le2msq  9866  msq11  9867  fimaxre  9911  lbreu  9914  infm3  9923  dfinfmr  9941  creur  9950  creui  9951  cju  9952  nnmulcl  9979  nndivtr  9997  avgle1  10163  avgle2  10164  avgle  10165  nn0nnaddcl  10208  zrevaddcl  10277  znnsub  10278  znn0sub  10279  zextlt  10300  gtndiv  10303  prime  10306  uztrn2  10459  uztric  10463  uz11  10464  uzwo  10495  uzwoOLD  10496  zmax  10527  zbtwnre  10528  rebtwnz  10529  qrevaddcl  10552  rpnnen1lem1  10556  rpnnen1lem2  10557  rpnnen1lem3  10558  rpnnen1lem5  10560  difrp  10601  xrltnsym  10686  xrlttri  10688  xrleloe  10693  xrletri  10700  xrletri3  10701  xrmaxeq  10723  xrmineq  10724  xrmaxlt  10725  xrmaxle  10727  z2ge  10740  qbtwnre  10741  qextlt  10745  qextle  10746  xleneg  10760  xaddcom  10780  xmulcom  10801  xmulneg2  10805  xmulgt0  10818  xrsupsslem  10841  xrinfmsslem  10842  supxrunb1  10854  supxrunb2  10855  ixxssixx  10886  ixxin  10889  ioon0  10898  iccid  10917  iooshf  10945  iccsupr  10953  iooneg  10973  iccneg  10974  iccsplit  10985  fzen  11028  fzass4  11046  fzrev  11064  fznn  11070  elfzm1b  11080  fzm1  11082  fzon  11113  fllt  11170  flbi  11178  flbi2  11179  flzadd  11183  modcyc2  11232  om2uzlt2i  11246  om2uzf1oi  11248  fseqsupubi  11272  expcllem  11347  faclbnd5  11544  hashbnd  11579  hasheni  11587  hasheqf1oi  11590  hashdom  11608  hashfacen  11658  ccatass  11705  ccatco  11759  shftlem  11838  shftuz  11839  shftfval  11840  shftval4  11847  shftval5  11848  2shfti  11850  seqshft  11855  mulre  11881  sqrlt  12022  abs3dif  12090  abs2difabs  12093  uzin2  12103  rexanre  12105  caubnd  12117  climshftlem  12323  rlimcn2  12339  fsumcnv  12512  geo2lim  12607  efle  12674  reef11  12675  demoivre  12756  demoivreALT  12757  sqr2irr  12803  0dvds  12825  muldvds1  12829  muldvds2  12830  dvdscmulr  12833  dvdssubr  12846  dvdsadd2b  12847  odd2np1  12863  divalglem9  12876  ndvdssub  12882  gcdcllem1  12966  gcdcom  12975  neggcd  12982  gcdabs2  12990  modgcd  12991  dvdsprm  13054  coprmdvds  13057  qredeq  13061  odzdvds  13136  coprimeprodsq  13138  pythagtriplem1  13145  pythagtriplem4  13148  pc2dvds  13207  pc11  13208  pcz  13209  pcprod  13219  prmunb  13237  1arithlem3  13248  1arith  13250  ressabs  13482  acsfn2  13843  issect  13934  pospo  14385  clatglbss  14509  pospropd  14516  pslem  14593  tsrss  14610  spweu  14614  issubmnd  14679  submcl  14708  resmhm2b  14716  frmdmnd  14759  frmd0  14760  grpinvsub  14826  gimcnv  15009  gimco  15010  gictr  15017  cntz2ss  15086  cntzrec  15087  dfod2  15155  lsmcom2  15244  efgred  15335  divsabl  15435  cygabl  15455  eldprd  15517  dfrhm2  15776  lmimcnv  16094  psrbagsuppfi  16520  cnfldexp  16689  cnsrng  16690  xrsdsreval  16698  dvdsrz  16722  znf1o  16787  ocvocv  16853  ocvin  16856  eltg  16977  eltg2  16978  tgss  16988  tgss2  17007  basgen2  17009  bastop1  17013  cldmre  17097  toponmre  17112  opnneiss  17137  restcldr  17192  restfpw  17197  restcls  17199  restntr  17200  ordtbaslem  17206  ordtrest2lem  17221  leordtvallem2  17229  leordtval  17231  cnrest  17303  t0sep  17342  cmpcov  17406  cmpsublem  17416  cmpsub  17417  2ndcomap  17474  ptval  17555  xkoval  17572  txss12  17590  ptrescn  17624  xkopt  17640  hmeofval  17743  txswaphmeolem  17789  txswaphmeo  17790  trfbas2  17828  trfbas  17829  uzrest  17882  numufl  17900  ssufl  17903  flimclsi  17963  hauspwpwf1  17972  ghmcnp  18097  blpnfctr  18419  metequiv  18492  metcnp3  18523  elbl4  18559  restmetu  18570  tngngp  18648  qtopbaslem  18745  bl2ioo  18776  ioo2bl  18777  ioo2blex  18778  xrsxmet  18793  divccn  18856  divccncf  18889  causs  19204  lmclim  19208  bcthlem1  19230  ovolfsf  19321  ioombl  19412  iccvolcl  19414  ioorcl  19422  volcn  19451  itg2itg1  19581  dvexp  19792  dvmptfsum  19812  dvexp3  19815  dvef  19817  dvlip  19830  c1lip1  19834  ftc1a  19874  tdeglem1  19934  tdeglem3  19935  tdeglem4  19936  coe1termlem  20129  plyremlem  20174  ptolemy  20357  cos11  20388  logeftb  20431  logleb  20451  logdivlt  20469  logdivle  20470  angval  20596  isppw2  20851  issqf  20872  vmasum  20953  lgsquadlem3  21093  ostth  21286  nb3graprlem2  21414  isspthonpth  21537  wlkdvspthlem  21560  3v3e3cycl1  21584  constr3trllem2  21591  constr3trllem3  21592  eupatrl  21643  ablomul  21896  isdivrngo  21972  vcz  22002  isvc  22013  isnv  22044  isnvi  22045  nmooge0  22221  nmblolbii  22253  blocnilem  22258  ipblnfi  22310  hvpncan2  22495  hvaddsub4  22533  hire  22549  abshicom  22556  hial2eq2  22562  orthcom  22563  hhssabloi  22715  ocsh  22738  shscli  22772  shscom  22774  shsel2  22777  spanss  22803  shjcom  22813  shmodsi  22844  chpsscon3  22958  spansni  23012  spansnmul  23019  spansncol  23023  spanunsni  23034  cmcm2  23071  cm2j  23075  spansncvi  23107  5oalem2  23110  3oalem2  23118  honegsubdi2  23267  adjsym  23289  cnvadj  23348  brafn  23403  kbpj  23412  riesz3i  23518  cnlnadjlem2  23524  cnlnadjlem9  23531  nmopcoi  23551  cnvbraval  23566  leop  23579  leop3  23581  leopmul2i  23591  leoptri  23592  hstrlem3a  23716  cvcon3  23740  cvnsym  23746  mdbr2  23752  dmdmd  23756  dmdbr2  23759  dmdbr3  23761  dmdbr4  23762  dmdbr5  23764  mdsl0  23766  ssmd2  23768  mdslmd1lem1  23781  mdslmd1lem2  23782  mdslmd3i  23788  mdslmd4i  23789  atcveq0  23804  superpos  23810  atnemeq0  23833  atssma  23834  atexch  23837  atomli  23838  atcvatlem  23841  atcvati  23842  chirredlem1  23846  chirredlem3  23848  chirredi  23850  atcvat3i  23852  atdmd  23854  mdsymlem1  23859  mdsymlem3  23861  mdsymlem4  23862  mdsymlem5  23863  mdsymlem8  23866  dmdsym  23869  atdmd2  23870  sumdmdlem  23874  cdjreui  23888  cdj3lem2b  23893  cdj3i  23897  imadifxp  23991  abfmpel  24020  xaddeq0  24072  xrofsup  24079  xeqlelt  24092  xdivpnfrp  24132  xrsinvgval  24152  xrsmulgzz  24153  cnvordtrestixx  24264  indval  24364  esumpfinvallem  24417  sigagenss  24485  brae  24545  dya2iocival  24576  dya2iocnei  24585  dya2iocuni  24586  derangenlem  24810  subfacval2  24826  kur14  24855  elfzp1b  25069  lediv2aALT  25070  mulsuble0b  25146  ntrivcvgfvn0  25180  prodmo  25215  zprod  25216  prodss  25226  fprodcnv  25260  faclim2  25315  funpsstri  25335  setlikespec  25401  dftrpred3g  25450  soseq  25468  wfr3g  25469  wfrlem5  25474  wfrlem10  25479  frrlem5  25499  elno  25514  sltsolem1  25536  nodenselem4  25552  nofulllem5  25574  brbtwn2  25748  colinearalglem4  25752  ax5seglem1  25771  ax5seglem2  25772  axcontlem2  25808  axcontlem12  25818  bpolysum  26003  bpoly4  26009  hfelhf  26026  onsuct0  26095  nndivsub  26111  ltflcei  26140  leceifl  26141  lxflflp1  26142  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  cnambfre  26154  itg2addnclem2  26156  itg2addnc  26158  itg2gt0cn  26159  elicc3  26210  nn0prpwlem  26215  nn0prpw  26216  isfne  26238  locfincmp  26274  unirep  26304  opelopab3  26308  fvopabf4g  26312  indexa  26325  filbcmb  26332  fzadd2  26335  incsequz2  26343  metf1o  26351  sstotbnd3  26375  isbnd2  26382  bndss  26385  ismtycnv  26401  iccbnd  26439  exidreslem  26442  exidresid  26444  ghomco  26448  isdrngo2  26464  rngoisocnv  26487  riscer  26494  crngohomfo  26506  unichnidl  26531  maxidlmax  26543  igenmin  26564  prtlem16  26608  ismrc  26645  nacsfg  26649  isnacs3  26654  incssnn0  26655  elmapssres  26661  mzpclall  26674  lerabdioph  26755  ltrabdioph  26758  eldioph4b  26762  jm2.17b  26916  congrep  26928  unxpwdom3  27124  islindf  27150  lindff  27153  lindfrn  27159  f1lindf  27160  lnr2i  27188  pmtrfinv  27270  mamudir  27330  matsca2  27342  matbas2  27343  matlmod  27347  expgrowth  27420  2sbc6g  27483  2sbc5g  27484  ordpss  27521  addrcom  27547  fmul01  27577  ioovolcl  27609  stoweidlem34  27650  sigarac  27709  2reu3  27833  afv0nbfvbi  27882  dmfcoafv  27906  ubmelm1fzo  27987  swrdltnd  28000  swrdccatin12lem3b  28022  swrdccatin12lem3  28024  swrdccatin12  28026  frgra3v  28106  frgraregorufr  28156  usg2spot2nb  28168  3impcombi  28638  sspwimp  28739  sspwimpVD  28740  a9e2ndeqALT  28753  bnj934  29012  paddss1  30299  paddss2  30300  paddss12  30301  pclfinN  30382  erngmul-rN  31296  mapdordlem2  32120
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