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  1588  nfeud2  2188  2eu1  2256  2eu3  2258  eqeqan12rd  2332  sylan9eqr  2370  morex  2983  sbcrext  3098  sylan9ssr  3227  pssdifcom1  3573  pssdifcom2  3574  riinn0  4013  breqan12rd  4076  ordelssne  4456  ordtri3or  4461  ordtri2  4464  ordtri4  4466  ordtr2  4473  ordtr3  4474  ordintdif  4478  ordtri2or  4525  dfwe2  4610  ordsucelsuc  4650  ordunisuc2  4672  tfindsg  4688  tfindsg2  4689  dfom2  4695  soinxp  4791  frinxp  4792  seinxp  4793  brelrng  4945  dminss  5132  imainss  5133  funsng  5335  funcnvuni  5354  f1co  5484  f1ocnv  5523  fun11iun  5531  f1oprswap  5553  funimass4  5611  dffv2  5630  fndmdifcom  5668  fsn2  5736  fvtp2  5764  fvtp3  5765  cofunex2g  5781  soisoi  5867  oveqan12rd  5920  curry2  6255  soxp  6270  tposoprab  6312  brrpssg  6321  sorpsscmpl  6330  smores3  6412  smores2  6413  smoel  6419  tfr3  6457  tz7.48-2  6496  tz7.49  6499  oaordi  6586  oaword  6589  oaord1  6591  oaword2  6593  oa00  6599  oalimcl  6600  oaass  6601  oarec  6602  oacomf1o  6605  omord2  6607  omcan  6609  omword  6610  omword1  6613  omword2  6614  odi  6619  omass  6620  oneo  6621  oen0  6626  oecan  6629  oelim2  6635  nnarcl  6656  nnaordi  6658  nnaordr  6660  nnawordi  6661  nnmsucr  6665  nnmcom  6666  nnaword  6667  nnmordi  6671  nnaordex  6678  oaabslem  6683  omabslem  6686  nnneo  6691  omsmo  6694  ersym  6714  elecg  6740  riiner  6774  ecopovsym  6803  ecovcom  6812  mapvalg  6825  pmvalg  6826  elpmg  6829  pmss12g  6837  ixpconstg  6868  ener  6951  domtr  6957  f1imaeng  6964  fundmen  6977  xpcomco  6995  xpsnen2g  6998  xpdom2  7000  xpdom1g  7002  omxpen  7007  omf1o  7008  enen2  7045  domen2  7047  sdomen2  7049  domtriord  7050  sdomel  7051  onsdominel  7053  infensuc  7082  onomeneq  7093  nndomo  7097  pssnn  7124  unbnn  7158  infcntss  7175  fiint  7178  mapfi  7197  fiin  7220  fiss  7222  oiiso  7297  unwdomg  7343  suc11reg  7365  inf3lem5  7378  infeq5  7383  cantnfp1lem3  7427  r1tr  7493  r1val1  7503  rankr1ai  7515  rankonidlem  7545  onssr1  7548  tskwe  7628  carddom2  7655  carden2  7665  domtri2  7667  cardval2  7669  fidomtri  7671  fidomtri2  7672  harval2  7675  dif1card  7683  infxpenlem  7686  ac5num  7708  alephord3  7750  alephdom  7753  aleph11  7756  alephdom2  7759  cardaleph  7761  dfac3  7793  dfac5  7800  cdacomen  7852  onacda  7868  pwsdompw  7875  ackbij1lem11  7901  ackbij2  7914  cfeq0  7927  cfsuc  7928  cff1  7929  cflim2  7934  cfsmolem  7941  coftr  7944  sornom  7948  infpssrlem4  7977  ssfin4  7981  ssfin2  7991  ssfin3ds  8001  fin23lem31  8014  isf32lem9  8032  hsmexlem5  8101  axdc3lem  8121  axdc3lem2  8122  axdc3lem4  8124  zorn2lem6  8173  brdom3  8198  brdom7disj  8201  brdom6disj  8202  alephval2  8239  alephreg  8249  wuncss  8412  gruen  8479  addcompi  8563  mulcompi  8565  ltapi  8572  ltmpi  8573  nqereu  8598  addcompq  8619  addcomnq  8620  mulcompq  8621  mulcomnq  8622  ltsonq  8638  ltanq  8640  ltmnq  8641  genpnnp  8674  addcompr  8690  mulcompr  8692  ltsopr  8701  ltexprlem2  8706  prlem936  8716  suplem2pr  8722  map2psrpr  8777  axpre-ltadd  8834  xrltnle  8936  axlttri  8939  axsup  8943  ltnle  8947  letri3  8952  leloe  8953  eqlelt  8954  letric  8966  mul31  9025  subcl  9096  pncan2  9103  pncan3  9104  npcan  9105  addsubeq4  9111  npncan3  9130  negsubdi2  9151  muladd  9257  subdi  9258  mulneg2  9262  mulsub  9267  ltleadd  9302  ltsubpos  9311  posdif  9312  addge01  9329  lesub0  9335  wloglei  9350  prodgt02  9647  prodge02  9649  ltdivmul  9673  ledivmul  9674  lt2mul2div  9677  lerec  9683  lt2msq  9685  ltdiv23  9692  lediv23  9693  lediv2a  9695  le2msq  9701  msq11  9702  fimaxre  9746  lbreu  9749  infm3  9758  dfinfmr  9776  creur  9785  creui  9786  cju  9787  nnmulcl  9814  nndivtr  9832  avgle1  9998  avgle2  9999  avgle  10000  nn0nnaddcl  10043  zrevaddcl  10110  znnsub  10111  znn0sub  10112  zextlt  10133  gtndiv  10136  prime  10139  uztrn2  10292  uztric  10296  uz11  10297  uzwo  10328  uzwoOLD  10329  zmax  10360  zbtwnre  10361  rebtwnz  10362  qrevaddcl  10385  rpnnen1lem1  10389  rpnnen1lem2  10390  rpnnen1lem3  10391  rpnnen1lem5  10393  difrp  10434  xrltnsym  10518  xrlttri  10520  xrleloe  10525  xrletri  10532  xrletri3  10533  xrmaxeq  10555  xrmineq  10556  xrmaxlt  10557  xrmaxle  10559  z2ge  10572  qbtwnre  10573  qextlt  10577  qextle  10578  xleneg  10592  xaddcom  10612  xmulcom  10633  xmulneg2  10637  xmulgt0  10650  xrsupsslem  10672  xrinfmsslem  10673  supxrunb1  10685  supxrunb2  10686  ixxssixx  10717  ixxin  10720  ioon0  10729  iccid  10748  iooshf  10775  iccsupr  10783  iooneg  10803  iccneg  10804  iccsplit  10815  fzen  10858  fzass4  10876  fzrev  10893  fznn  10899  elfzm1b  10907  fzm1  10909  fllt  10985  flbi  10993  flbi2  10994  flzadd  10998  modcyc2  11047  om2uzlt2i  11061  om2uzf1oi  11063  fseqsupubi  11087  expcllem  11161  faclbnd5  11358  hashbnd  11390  hasheni  11394  hashdom  11408  hashfacen  11439  ccatass  11483  ccatco  11537  shftlem  11610  shftuz  11611  shftfval  11612  shftval4  11619  shftval5  11620  2shfti  11622  seqshft  11627  mulre  11653  sqrlt  11794  abs3dif  11862  abs2difabs  11865  uzin2  11875  rexanre  11877  caubnd  11889  climshftlem  12095  rlimcn2  12111  fsumcnv  12283  geo2lim  12378  efle  12445  reef11  12446  demoivre  12527  demoivreALT  12528  sqr2irr  12574  0dvds  12596  muldvds1  12600  muldvds2  12601  dvdscmulr  12604  dvdssubr  12617  dvdsadd2b  12618  odd2np1  12634  divalglem9  12647  ndvdssub  12653  gcdcllem1  12737  gcdcom  12746  neggcd  12753  gcdabs2  12761  modgcd  12762  dvdsprm  12825  coprmdvds  12828  qredeq  12832  odzdvds  12907  coprimeprodsq  12909  pythagtriplem1  12916  pythagtriplem4  12919  pc2dvds  12978  pc11  12979  pcz  12980  pcprod  12990  prmunb  13008  1arithlem3  13019  1arith  13021  ressabs  13253  acsfn2  13614  issect  13705  pospo  14156  clatglbss  14280  pospropd  14287  pslem  14364  tsrss  14381  spweu  14385  issubmnd  14450  submcl  14479  resmhm2b  14487  frmdmnd  14530  frmd0  14531  grpinvsub  14597  gimcnv  14780  gimco  14781  gictr  14788  cntz2ss  14857  cntzrec  14858  dfod2  14926  lsmcom2  15015  efgred  15106  divsabl  15206  cygabl  15226  eldprd  15288  dfrhm2  15547  lmimcnv  15869  psrbagsuppfi  16295  cnfldexp  16463  cnsrng  16464  xrsdsreval  16472  dvdsrz  16496  znf1o  16561  ocvocv  16627  ocvin  16630  eltg  16751  eltg2  16752  tgss  16762  tgss2  16781  basgen2  16783  bastop1  16787  cldmre  16871  toponmre  16886  opnneiss  16911  restcldr  16961  restfpw  16966  restcls  16967  restntr  16968  ordtbaslem  16974  ordtrest2lem  16989  leordtvallem2  16997  leordtval  16999  cnrest  17069  t0sep  17108  cmpcov  17172  cmpsublem  17182  cmpsub  17183  2ndcomap  17240  ptval  17321  xkoval  17338  txss12  17356  ptrescn  17389  xkopt  17405  hmeofval  17505  txswaphmeolem  17551  txswaphmeo  17552  trfbas2  17590  trfbas  17591  uzrest  17644  numufl  17662  ssufl  17665  flimclsi  17725  hauspwpwf1  17734  ghmcnp  17849  blpnfctr  18034  metequiv  18107  metcnp3  18138  tngngp  18222  qtopbaslem  18319  bl2ioo  18350  ioo2bl  18351  ioo2blex  18352  xrsxmet  18367  divccn  18429  divccncf  18462  causs  18777  lmclim  18781  bcthlem1  18799  ovolfsf  18884  ioombl  18975  iccvolcl  18977  ioorcl  18985  volcn  19014  itg2itg1  19144  dvexp  19355  dvmptfsum  19375  dvexp3  19378  dvef  19380  dvlip  19393  c1lip1  19397  ftc1a  19437  tdeglem1  19497  tdeglem3  19498  tdeglem4  19499  coe1termlem  19692  plyremlem  19737  ptolemy  19917  cos11  19948  logeftb  19990  logleb  20010  logdivlt  20025  logdivle  20026  angval  20152  isppw2  20406  issqf  20427  vmasum  20508  lgsquadlem3  20648  ostth  20841  ablomul  21075  isdivrngo  21151  vcz  21181  isvc  21192  isnv  21223  isnvi  21224  nmooge0  21400  nmblolbii  21432  blocnilem  21437  ipblnfi  21489  hvpncan2  21674  hvaddsub4  21712  hire  21728  abshicom  21735  hial2eq2  21741  orthcom  21742  hhssabloi  21894  ocsh  21917  shscli  21951  shscom  21953  shsel2  21956  spanss  21982  shjcom  21992  shmodsi  22023  chpsscon3  22137  spansni  22191  spansnmul  22198  spansncol  22202  spanunsni  22213  cmcm2  22250  cm2j  22254  spansncvi  22286  5oalem2  22289  3oalem2  22297  honegsubdi2  22446  adjsym  22468  cnvadj  22527  brafn  22582  kbpj  22591  riesz3i  22697  cnlnadjlem2  22703  cnlnadjlem9  22710  nmopcoi  22730  cnvbraval  22745  leop  22758  leop3  22760  leopmul2i  22770  leoptri  22771  hstrlem3a  22895  cvcon3  22919  cvnsym  22925  mdbr2  22931  dmdmd  22935  dmdbr2  22938  dmdbr3  22940  dmdbr4  22941  dmdbr5  22943  mdsl0  22945  ssmd2  22947  mdslmd1lem1  22960  mdslmd1lem2  22961  mdslmd3i  22967  mdslmd4i  22968  atcveq0  22983  superpos  22989  atnemeq0  23012  atssma  23013  atexch  23016  atomli  23017  atcvatlem  23020  atcvati  23021  chirredlem1  23025  chirredlem3  23027  chirredi  23029  atcvat3i  23031  atdmd  23033  mdsymlem1  23038  mdsymlem3  23040  mdsymlem4  23041  mdsymlem5  23042  mdsymlem8  23045  dmdsym  23048  atdmd2  23049  sumdmdlem  23053  cdjreui  23067  cdj3lem2b  23072  cdj3i  23076  r19.29_2a  23104  imadifxp  23187  abfmpel  23216  xrofsup  23272  xeqlelt  23286  xdivpnfrp  23332  xaddeq0  23339  cnvordtrestixx  23380  restmetu  23513  esumpfinvallem  23640  sigaclci  23691  sigagenss  23708  brae  23766  dya2iocival  23797  dya2iocnei  23806  dya2iocuni  23807  indval  23826  derangenlem  23986  subfacval2  24002  kur14  24031  elfzp1b  24296  lediv2aALT  24297  mulsuble0b  24374  ntrivcvgfvn0  24404  prodmo  24439  zprod  24440  prodss  24450  faclimlem3  24483  faclim2  24486  funpsstri  24506  setlikespec  24572  dftrpred3g  24621  soseq  24639  wfr3g  24640  wfrlem5  24645  wfrlem10  24650  frrlem5  24670  elno  24685  sltsolem1  24707  nodenselem4  24723  nofulllem5  24745  brbtwn2  24919  colinearalglem4  24923  ax5seglem1  24942  ax5seglem2  24943  axcontlem2  24979  axcontlem12  24989  bpolysum  25174  bpoly4  25180  hfelhf  25197  onsuct0  25266  nndivsub  25282  ltflcei  25312  leceifl  25313  lxflflp1  25314  ovoliunnfl  25315  itg2addnclem2  25318  itg2gt0cn  25320  elicc3  25377  nn0prpwlem  25387  nn0prpw  25388  isfne  25417  locfincmp  25453  unirep  25498  opelopab3  25522  fvopabf4g  25535  indexa  25561  filbcmb  25581  fzadd2  25593  incsequz2  25608  lpss2  25617  metf1o  25618  sstotbnd3  25648  isbnd2  25655  bndss  25658  ismtycnv  25674  iccbnd  25712  exidreslem  25715  exidresid  25717  ghomco  25721  isdrngo2  25737  rngoisocnv  25760  riscer  25767  crngohomfo  25779  unichnidl  25804  maxidlmax  25816  igenmin  25837  prtlem16  25885  ismrc  25924  nacsfg  25928  isnacs3  25933  incssnn0  25934  elmapssres  25940  mzpclall  25953  lerabdioph  26034  ltrabdioph  26037  eldioph4b  26042  jm2.17b  26196  congrep  26208  unxpwdom3  26404  islindf  26430  lindff  26433  lindfrn  26439  f1lindf  26440  lnr2i  26468  pmtrfinv  26550  mamudir  26610  matsca2  26622  matbas2  26623  matlmod  26627  expgrowth  26700  2sbc6g  26763  2sbc5g  26764  ordpss  26802  addrcom  26828  fmul01  26858  ioovolcl  26890  stoweidlem34  26931  sigarac  26990  2reu3  27114  afv0nbfvbi  27164  dmfcoafv  27188  fvtp2g  27238  fvtp3g  27239  mpt2xopoveqd  27261  fzon  27274  hasheqf1oi  27290  nb3graprlem2  27398  wlkdvspthlem  27503  eupatrl  27523  usgrcyclnl1  27524  3v3e3cycl1  27528  constr3trllem2  27535  constr3trllem3  27536  frgra3v  27594  biimpa21  27829  3impcombi  28101  sspwimp  28205  sspwimpVD  28206  a9e2ndeqALT  28219  bnj934  28478  paddss1  29824  paddss2  29825  paddss12  29826  pclfinN  29907  erngmul-rN  30821  mapdordlem2  31645
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