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  1584  nfeud2  2155  2eu1  2223  2eu3  2225  eqeqan12rd  2299  sylan9eqr  2337  morex  2949  sbcrext  3064  sylan9ssr  3193  pssdifcom1  3539  pssdifcom2  3540  riinn0  3976  breqan12rd  4039  ordelssne  4419  ordtri3or  4424  ordtri2  4427  ordtri4  4429  ordtr2  4436  ordtr3  4437  ordintdif  4441  ordtri2or  4488  dfwe2  4573  ordsucelsuc  4613  ordunisuc2  4635  tfindsg  4651  tfindsg2  4652  dfom2  4658  soinxp  4754  frinxp  4755  seinxp  4756  brelrng  4908  dminss  5095  imainss  5096  funsng  5298  funcnvuni  5317  f1co  5446  f1ocnv  5485  fun11iun  5493  f1oprswap  5515  funimass4  5573  dffv2  5592  fndmdifcom  5630  fsn2  5698  fvtp2  5725  fvtp3  5726  cofunex2g  5740  soisoi  5825  oveqan12rd  5878  curry2  6213  soxp  6228  tposoprab  6270  brrpssg  6279  sorpsscmpl  6288  smores3  6370  smores2  6371  smoel  6377  tfr3  6415  tz7.48-2  6454  tz7.49  6457  oaordi  6544  oaword  6547  oaord1  6549  oaword2  6551  oa00  6557  oalimcl  6558  oaass  6559  oarec  6560  oacomf1o  6563  omord2  6565  omcan  6567  omword  6568  omword1  6571  omword2  6572  odi  6577  omass  6578  oneo  6579  oen0  6584  oecan  6587  oelim2  6593  nnarcl  6614  nnaordi  6616  nnaordr  6618  nnawordi  6619  nnmsucr  6623  nnmcom  6624  nnaword  6625  nnmordi  6629  nnaordex  6636  oaabslem  6641  omabslem  6644  nnneo  6649  omsmo  6652  ersym  6672  elecg  6698  riiner  6732  ecopovsym  6760  ecovcom  6769  mapvalg  6782  pmvalg  6783  elpmg  6786  pmss12g  6794  ixpconstg  6825  ener  6908  domtr  6914  f1imaeng  6921  fundmen  6934  xpcomco  6952  xpsnen2g  6955  xpdom2  6957  xpdom1g  6959  omxpen  6964  omf1o  6965  enen2  7002  domen2  7004  sdomen2  7006  domtriord  7007  sdomel  7008  onsdominel  7010  infensuc  7039  onomeneq  7050  nndomo  7054  pssnn  7081  unbnn  7113  infcntss  7130  fiint  7133  mapfi  7152  fiin  7175  fiss  7177  oiiso  7252  unwdomg  7298  suc11reg  7320  inf3lem5  7333  infeq5  7338  cantnfp1lem3  7382  r1tr  7448  r1val1  7458  rankr1ai  7470  rankonidlem  7500  onssr1  7503  tskwe  7583  carddom2  7610  carden2  7620  domtri2  7622  cardval2  7624  fidomtri  7626  fidomtri2  7627  harval2  7630  dif1card  7638  infxpenlem  7641  ac5num  7663  alephord3  7705  alephdom  7708  aleph11  7711  alephdom2  7714  cardaleph  7716  dfac3  7748  dfac5  7755  cdacomen  7807  onacda  7823  pwsdompw  7830  ackbij1lem11  7856  ackbij2  7869  cfeq0  7882  cfsuc  7883  cff1  7884  cflim2  7889  cfsmolem  7896  coftr  7899  sornom  7903  infpssrlem4  7932  ssfin4  7936  ssfin2  7946  ssfin3ds  7956  fin23lem31  7969  isf32lem9  7987  hsmexlem5  8056  axdc3lem  8076  axdc3lem2  8077  axdc3lem4  8079  zorn2lem6  8128  brdom3  8153  brdom7disj  8156  brdom6disj  8157  alephval2  8194  alephreg  8204  wuncss  8367  gruen  8434  addcompi  8518  mulcompi  8520  ltapi  8527  ltmpi  8528  nqereu  8553  addcompq  8574  addcomnq  8575  mulcompq  8576  mulcomnq  8577  ltsonq  8593  ltanq  8595  ltmnq  8596  genpnnp  8629  addcompr  8645  mulcompr  8647  ltsopr  8656  ltexprlem2  8661  prlem936  8671  suplem2pr  8677  map2psrpr  8732  axpre-ltadd  8789  xrltnle  8891  axlttri  8894  axsup  8898  ltnle  8902  letri3  8907  leloe  8908  eqlelt  8909  letric  8921  mul31  8980  subcl  9051  pncan2  9058  pncan3  9059  npcan  9060  addsubeq4  9066  npncan3  9085  negsubdi2  9106  muladd  9212  subdi  9213  mulneg2  9217  mulsub  9222  ltleadd  9257  ltsubpos  9266  posdif  9267  addge01  9284  lesub0  9290  wloglei  9305  prodgt02  9602  prodge02  9604  ltdivmul  9628  ledivmul  9629  lt2mul2div  9632  lerec  9638  lt2msq  9640  ltdiv23  9647  lediv23  9648  lediv2a  9650  le2msq  9656  msq11  9657  fimaxre  9701  lbreu  9704  infm3  9713  dfinfmr  9731  creur  9740  creui  9741  cju  9742  nnmulcl  9769  nndivtr  9787  avgle1  9951  avgle2  9952  avgle  9953  nn0nnaddcl  9996  zrevaddcl  10063  znnsub  10064  znn0sub  10065  zextlt  10086  gtndiv  10089  prime  10092  uztrn2  10245  uztric  10249  uz11  10250  uzwo  10281  uzwoOLD  10282  zmax  10313  zbtwnre  10314  rebtwnz  10315  qrevaddcl  10338  rpnnen1lem1  10342  rpnnen1lem2  10343  rpnnen1lem3  10344  rpnnen1lem5  10346  difrp  10387  xrltnsym  10471  xrlttri  10473  xrleloe  10478  xrletri  10485  xrletri3  10486  xrmaxeq  10508  xrmineq  10509  xrmaxlt  10510  xrmaxle  10512  z2ge  10525  qbtwnre  10526  qextlt  10530  qextle  10531  xleneg  10545  xaddcom  10565  xmulcom  10586  xmulneg2  10590  xmulgt0  10603  xrsupsslem  10625  xrinfmsslem  10626  supxrunb1  10638  supxrunb2  10639  ixxssixx  10670  ixxin  10673  ioon0  10682  iccid  10701  iooshf  10728  iccsupr  10736  iooneg  10756  iccneg  10757  iccsplit  10768  fzen  10811  fzass4  10829  fzrev  10846  fznn  10852  elfzm1b  10860  fzm1  10862  fllt  10938  flbi  10946  flbi2  10947  flzadd  10951  modcyc2  11000  om2uzlt2i  11014  om2uzf1oi  11016  fseqsupubi  11040  expcllem  11114  faclbnd5  11311  hashbnd  11343  hasheni  11347  hashdom  11361  hashfacen  11392  ccatass  11436  ccatco  11490  shftlem  11563  shftuz  11564  shftfval  11565  shftval4  11572  shftval5  11573  2shfti  11575  seqshft  11580  mulre  11606  sqrlt  11747  abs3dif  11815  abs2difabs  11818  uzin2  11828  rexanre  11830  caubnd  11842  climshftlem  12048  rlimcn2  12064  fsumcnv  12236  geo2lim  12331  efle  12398  reef11  12399  demoivre  12480  demoivreALT  12481  sqr2irr  12527  0dvds  12549  muldvds1  12553  muldvds2  12554  dvdscmulr  12557  dvdssubr  12570  dvdsadd2b  12571  odd2np1  12587  divalglem9  12600  ndvdssub  12606  gcdcllem1  12690  gcdcom  12699  neggcd  12706  gcdabs2  12714  modgcd  12715  dvdsprm  12778  coprmdvds  12781  qredeq  12785  odzdvds  12860  coprimeprodsq  12862  pythagtriplem1  12869  pythagtriplem4  12872  pc2dvds  12931  pc11  12932  pcz  12933  pcprod  12943  prmunb  12961  1arithlem3  12972  1arith  12974  ressabs  13206  acsfn2  13565  issect  13656  pospo  14107  clatglbss  14231  pospropd  14238  pslem  14315  tsrss  14332  spweu  14336  issubmnd  14401  submcl  14430  resmhm2b  14438  frmdmnd  14481  frmd0  14482  grpinvsub  14548  gimcnv  14731  gimco  14732  gictr  14739  cntz2ss  14808  cntzrec  14809  dfod2  14877  lsmcom2  14966  efgred  15057  divsabl  15157  cygabl  15177  eldprd  15239  dfrhm2  15498  lmimcnv  15820  psrbagsuppfi  16246  cnfldexp  16407  cnsrng  16408  xrsdsreval  16416  dvdsrz  16440  znf1o  16505  ocvocv  16571  ocvin  16574  eltg  16695  eltg2  16696  tgss  16706  tgss2  16725  basgen2  16727  bastop1  16731  cldmre  16815  toponmre  16830  opnneiss  16855  restcldr  16905  restfpw  16910  restcls  16911  restntr  16912  ordtbaslem  16918  ordtrest2lem  16933  leordtvallem2  16941  leordtval  16943  cnrest  17013  t0sep  17052  cmpcov  17116  cmpsublem  17126  cmpsub  17127  2ndcomap  17184  ptval  17265  xkoval  17282  txss12  17300  ptrescn  17333  xkopt  17349  hmeofval  17449  txswaphmeolem  17495  txswaphmeo  17496  trfbas2  17538  trfbas  17539  uzrest  17592  numufl  17610  ssufl  17613  flimclsi  17673  hauspwpwf1  17682  ghmcnp  17797  blpnfctr  17982  metequiv  18055  metcnp3  18086  tngngp  18170  qtopbaslem  18267  bl2ioo  18298  ioo2bl  18299  ioo2blex  18300  xrsxmet  18315  divccn  18377  divccncf  18410  causs  18724  lmclim  18728  bcthlem1  18746  ovolfsf  18831  ioombl  18922  iccvolcl  18924  ioorcl  18932  volcn  18961  itg2itg1  19091  dvexp  19302  dvmptfsum  19322  dvexp3  19325  dvef  19327  dvlip  19340  c1lip1  19344  ftc1a  19384  tdeglem1  19444  tdeglem3  19445  tdeglem4  19446  coe1termlem  19639  plyremlem  19684  ptolemy  19864  cos11  19895  logeftb  19937  logleb  19957  logdivlt  19972  logdivle  19973  angval  20099  isppw2  20353  issqf  20374  vmasum  20455  lgsquadlem3  20595  ostth  20788  ablomul  21022  isdivrngo  21098  vcz  21126  isvc  21137  isnv  21168  isnvi  21169  nmooge0  21345  nmblolbii  21377  blocnilem  21382  ipblnfi  21434  hvpncan2  21619  hvaddsub4  21657  hire  21673  abshicom  21680  hial2eq2  21686  orthcom  21687  hhssabloi  21839  ocsh  21862  shscli  21896  shscom  21898  shsel2  21901  spanss  21927  shjcom  21937  shmodsi  21968  chpsscon3  22082  spansni  22136  spansnmul  22143  spansncol  22147  spanunsni  22158  cmcm2  22195  cm2j  22199  spansncvi  22231  5oalem2  22234  3oalem2  22242  honegsubdi2  22391  adjsym  22413  cnvadj  22472  brafn  22527  kbpj  22536  riesz3i  22642  cnlnadjlem2  22648  cnlnadjlem9  22655  nmopcoi  22675  cnvbraval  22690  leop  22703  leop3  22705  leopmul2i  22715  leoptri  22716  hstrlem3a  22840  cvcon3  22864  cvnsym  22870  mdbr2  22876  dmdmd  22880  dmdbr2  22883  dmdbr3  22885  dmdbr4  22886  dmdbr5  22888  mdsl0  22890  ssmd2  22892  mdslmd1lem1  22905  mdslmd1lem2  22906  mdslmd3i  22912  mdslmd4i  22913  atcveq0  22928  superpos  22934  atnemeq0  22957  atssma  22958  atexch  22961  atomli  22962  atcvatlem  22965  atcvati  22966  chirredlem1  22970  chirredlem3  22972  chirredi  22974  atcvat3i  22976  atdmd  22978  mdsymlem1  22983  mdsymlem3  22985  mdsymlem4  22986  mdsymlem5  22987  mdsymlem8  22990  dmdsym  22993  atdmd2  22994  sumdmdlem  22998  cdjreui  23012  cdj3lem2b  23017  cdj3i  23021  xdivpnfrp  23117  abfmpel  23219  xrofsup  23255  xeqlelt  23269  cnvordtrestixx  23297  xaddeq0  23304  esumpfinvallem  23442  sigaclci  23493  sigagenss  23510  dya2iocival  23576  indval  23597  derangenlem  23702  subfacval2  23718  kur14  23747  elfzp1b  24012  lediv2aALT  24013  mulsuble0b  24088  funpsstri  24121  setlikespec  24187  dftrpred3g  24236  soseq  24254  wfr3g  24255  wfrlem5  24260  wfrlem10  24265  frrlem5  24285  elno  24300  sltsolem1  24322  nodenselem4  24338  nofulllem5  24360  brbtwn2  24533  colinearalglem4  24537  ax5seglem1  24556  ax5seglem2  24557  axcontlem2  24593  axcontlem12  24603  bpolysum  24788  bpoly4  24794  hfelhf  24811  onsuct0  24880  nndivsub  24896  mappow  25089  celsor  25111  ffvelrnb  25131  mapex2  25140  injsurinj  25149  ubpar  25261  ranncnt  25283  tolat  25286  nelioo5  25511  hmeogrpi  25536  intopcoaconlem3b  25538  cnfilca  25556  limptlimpr2lem1  25574  islimrs3  25581  msr4  25606  mslb1  25607  iintlem1  25610  trdom  25613  cnvtr  25616  lvsovso  25626  supexr  25631  claddrvr  25648  cnegvex2  25660  rnegvex2  25661  intvconlem1  25703  1ded  25738  tartarmap  25888  cardtar  25904  fnctartar3  25909  setiscat  25979  indcls2  25996  clscnc  26010  bsstrs  26146  elicc3  26228  nn0prpwlem  26238  nn0prpw  26239  isfne  26268  locfincmp  26304  unirep  26349  opelopab3  26373  fvopabf4g  26386  indexa  26412  filbcmb  26432  fzadd2  26444  incsequz2  26459  lpss2  26468  metf1o  26469  sstotbnd3  26500  isbnd2  26507  bndss  26510  ismtycnv  26526  iccbnd  26564  exidreslem  26567  exidresid  26569  ghomco  26573  isdrngo2  26589  rngoisocnv  26612  riscer  26619  crngohomfo  26631  unichnidl  26656  maxidlmax  26668  igenmin  26689  prtlem16  26737  ismrc  26776  nacsfg  26780  isnacs3  26785  incssnn0  26786  elmapssres  26792  mzpclall  26805  lerabdioph  26886  ltrabdioph  26889  eldioph4b  26894  jm2.17b  27048  congrep  27060  unxpwdom3  27256  islindf  27282  lindff  27285  lindfrn  27291  f1lindf  27292  lnr2i  27320  pmtrfinv  27402  mamudir  27462  matsca2  27474  matbas2  27475  matlmod  27479  expgrowth  27552  2sbc6g  27615  2sbc5g  27616  ordpss  27654  addrcom  27680  fmul01  27710  ioovolcl  27742  stoweidlem34  27783  sigarac  27842  2reu3  27966  afv0nbfvbi  28014  dmfcoafv  28036  mpt2xopoveqd  28087  frgra3v  28180  biimpa21  28335  sspwimp  28694  sspwimpVD  28695  a9e2ndeqALT  28708  bnj934  28967  paddss1  30006  paddss2  30007  paddss12  30008  pclfinN  30089  erngmul-rN  31003  mapdordlem2  31827
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