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  1607  dvelimf  2064  nfeud2  2292  2eu1  2360  2eu3  2362  eqeqan12rd  2451  sylan9eqr  2489  r19.29_2a  2844  morex  3110  sbcrext  3226  sylan9ssr  3354  pssdifcom1  3705  pssdifcom2  3706  riinn0  4157  breqan12rd  4220  ordelssne  4600  ordtri3or  4605  ordtri2  4608  ordtri4  4610  ordtr2  4617  ordtr3  4618  ordintdif  4622  ordtri2or  4668  dfwe2  4753  ordsucelsuc  4793  ordunisuc2  4815  tfindsg  4831  tfindsg2  4832  dfom2  4838  soinxp  4933  frinxp  4934  seinxp  4935  brelrng  5090  dminss  5277  imainss  5278  funsng  5488  funcnvuni  5509  f1co  5639  f1ocnv  5678  fun11iun  5686  f1oprswap  5708  funimass4  5768  dffv2  5787  fndmdifcom  5826  fsn2  5899  fvtp2  5931  fvtp3  5932  fvtp2g  5934  fvtp3g  5935  cofunex2g  5951  soisoi  6039  oveqan12rd  6092  curry2  6432  soxp  6450  mpt2xopoveqd  6463  tposoprab  6506  brrpssg  6515  sorpsscmpl  6524  smores3  6606  smores2  6607  smoel  6613  tfr3  6651  tz7.48-2  6690  tz7.49  6693  oaordi  6780  oaword  6783  oaord1  6785  oaword2  6787  oa00  6793  oalimcl  6794  oaass  6795  oarec  6796  oacomf1o  6799  omord2  6801  omcan  6803  omword  6804  omword1  6807  omword2  6808  odi  6813  omass  6814  oneo  6815  oen0  6820  oecan  6823  oelim2  6829  nnarcl  6850  nnaordi  6852  nnaordr  6854  nnawordi  6855  nnmsucr  6859  nnmcom  6860  nnaword  6861  nnmordi  6865  nnaordex  6872  oaabslem  6877  omabslem  6880  nnneo  6885  omsmo  6888  ersym  6908  elecg  6934  riiner  6968  ecopovsym  6997  ecovcom  7006  mapvalg  7019  pmvalg  7020  elpmg  7023  pmss12g  7031  ixpconstg  7062  ener  7145  domtr  7151  f1imaeng  7158  fundmen  7171  xpcomco  7189  xpsnen2g  7192  xpdom2  7194  xpdom1g  7196  omxpen  7201  omf1o  7202  enen2  7239  domen2  7241  sdomen2  7243  domtriord  7244  sdomel  7245  onsdominel  7247  infensuc  7276  onomeneq  7287  nndomo  7291  pssnn  7318  unbnn  7354  infcntss  7371  fiint  7374  mapfi  7394  fiin  7418  fiss  7420  oiiso  7495  unwdomg  7541  suc11reg  7563  inf3lem5  7576  infeq5  7581  cantnfp1lem3  7625  r1tr  7691  r1val1  7701  rankr1ai  7713  rankonidlem  7743  onssr1  7746  tskwe  7826  carddom2  7853  carden2  7863  domtri2  7865  cardval2  7867  fidomtri  7869  fidomtri2  7870  harval2  7873  dif1card  7881  infxpenlem  7884  ac5num  7906  alephord3  7948  alephdom  7951  aleph11  7954  alephdom2  7957  cardaleph  7959  dfac3  7991  dfac5  7998  cdacomen  8050  onacda  8066  pwsdompw  8073  ackbij1lem11  8099  ackbij2  8112  cfeq0  8125  cfsuc  8126  cff1  8127  cflim2  8132  cfsmolem  8139  coftr  8142  sornom  8146  infpssrlem4  8175  ssfin4  8179  ssfin2  8189  ssfin3ds  8199  fin23lem31  8212  isf32lem9  8230  hsmexlem5  8299  axdc3lem  8319  axdc3lem2  8320  axdc3lem4  8322  zorn2lem6  8370  brdom3  8395  brdom7disj  8398  brdom6disj  8399  alephval2  8436  alephreg  8446  wuncss  8609  gruen  8676  addcompi  8760  mulcompi  8762  ltapi  8769  ltmpi  8770  nqereu  8795  addcompq  8816  addcomnq  8817  mulcompq  8818  mulcomnq  8819  ltsonq  8835  ltanq  8837  ltmnq  8838  genpnnp  8871  addcompr  8887  mulcompr  8889  ltsopr  8898  ltexprlem2  8903  prlem936  8913  suplem2pr  8919  map2psrpr  8974  axpre-ltadd  9031  xrltnle  9133  axlttri  9136  axsup  9140  ltnle  9144  letri3  9149  leloe  9150  eqlelt  9151  letric  9163  mul31  9223  subcl  9294  pncan2  9301  pncan3  9302  npcan  9303  addsubeq4  9309  npncan3  9328  negsubdi2  9349  muladd  9455  subdi  9456  mulneg2  9460  mulsub  9465  ltleadd  9500  ltsubpos  9509  posdif  9510  addge01  9527  lesub0  9533  wloglei  9548  prodgt02  9845  prodge02  9847  ltdivmul  9871  ledivmul  9872  lt2mul2div  9875  lerec  9881  lt2msq  9883  ltdiv23  9890  lediv23  9891  lediv2a  9893  le2msq  9899  msq11  9900  fimaxre  9944  lbreu  9947  infm3  9956  dfinfmr  9974  creur  9983  creui  9984  cju  9985  nnmulcl  10012  nndivtr  10030  avgle1  10196  avgle2  10197  avgle  10198  nn0nnaddcl  10241  zrevaddcl  10310  znnsub  10311  znn0sub  10312  zextlt  10333  gtndiv  10336  prime  10339  uztrn2  10492  uztric  10496  uz11  10497  uzwo  10528  uzwoOLD  10529  zmax  10560  zbtwnre  10561  rebtwnz  10562  qrevaddcl  10585  rpnnen1lem1  10589  rpnnen1lem2  10590  rpnnen1lem3  10591  rpnnen1lem5  10593  difrp  10634  xrltnsym  10719  xrlttri  10721  xrleloe  10726  xrletri  10733  xrletri3  10734  xrmaxeq  10756  xrmineq  10757  xrmaxlt  10758  xrmaxle  10760  z2ge  10773  qbtwnre  10774  qextlt  10778  qextle  10779  xleneg  10793  xaddcom  10813  xmulcom  10834  xmulneg2  10838  xmulgt0  10851  xrsupsslem  10874  xrinfmsslem  10875  supxrunb1  10887  supxrunb2  10888  ixxssixx  10919  ixxin  10922  ioon0  10931  iccid  10950  iooshf  10978  iccsupr  10986  iooneg  11006  iccneg  11007  iccsplit  11018  fzen  11061  fzass4  11079  fzrev  11097  fznn  11103  elfzm1b  11113  fzm1  11115  fzon  11146  fllt  11203  flbi  11211  flbi2  11212  flzadd  11216  modcyc2  11265  om2uzlt2i  11279  om2uzf1oi  11281  fseqsupubi  11305  expcllem  11380  faclbnd5  11577  hashbnd  11612  hasheni  11620  hasheqf1oi  11623  hashdom  11641  hashfacen  11691  ccatass  11738  ccatco  11792  shftlem  11871  shftuz  11872  shftfval  11873  shftval4  11880  shftval5  11881  2shfti  11883  seqshft  11888  mulre  11914  sqrlt  12055  abs3dif  12123  abs2difabs  12126  uzin2  12136  rexanre  12138  caubnd  12150  climshftlem  12356  rlimcn2  12372  fsumcnv  12545  geo2lim  12640  efle  12707  reef11  12708  demoivre  12789  demoivreALT  12790  sqr2irr  12836  0dvds  12858  muldvds1  12862  muldvds2  12863  dvdscmulr  12866  dvdssubr  12879  dvdsadd2b  12880  odd2np1  12896  divalglem9  12909  ndvdssub  12915  gcdcllem1  12999  gcdcom  13008  neggcd  13015  gcdabs2  13023  modgcd  13024  dvdsprm  13087  coprmdvds  13090  qredeq  13094  odzdvds  13169  coprimeprodsq  13171  pythagtriplem1  13178  pythagtriplem4  13181  pc2dvds  13240  pc11  13241  pcz  13242  pcprod  13252  prmunb  13270  1arithlem3  13281  1arith  13283  ressabs  13515  acsfn2  13876  issect  13967  pospo  14418  clatglbss  14542  pospropd  14549  pslem  14626  tsrss  14643  spweu  14647  issubmnd  14712  submcl  14741  resmhm2b  14749  frmdmnd  14792  frmd0  14793  grpinvsub  14859  gimcnv  15042  gimco  15043  gictr  15050  cntz2ss  15119  cntzrec  15120  dfod2  15188  lsmcom2  15277  efgred  15368  divsabl  15468  cygabl  15488  eldprd  15550  dfrhm2  15809  lmimcnv  16127  psrbagsuppfi  16553  cnfldexp  16722  cnsrng  16723  xrsdsreval  16731  dvdsrz  16755  znf1o  16820  ocvocv  16886  ocvin  16889  eltg  17010  eltg2  17011  tgss  17021  tgss2  17040  basgen2  17042  bastop1  17046  cldmre  17130  toponmre  17145  opnneiss  17170  restcldr  17226  restfpw  17231  restcls  17233  restntr  17234  ordtbaslem  17240  ordtrest2lem  17255  leordtvallem2  17263  leordtval  17265  cnrest  17337  t0sep  17376  cmpcov  17440  cmpsublem  17450  cmpsub  17451  2ndcomap  17509  ptval  17590  xkoval  17607  txss12  17625  ptrescn  17659  xkopt  17675  hmeofval  17778  txswaphmeolem  17824  txswaphmeo  17825  trfbas2  17863  trfbas  17864  uzrest  17917  numufl  17935  ssufl  17938  flimclsi  17998  hauspwpwf1  18007  ghmcnp  18132  blpnfctr  18454  metequiv  18527  metcnp3  18558  elbl4  18594  restmetu  18605  tngngp  18683  qtopbaslem  18780  bl2ioo  18811  ioo2bl  18812  ioo2blex  18813  xrsxmet  18828  divccn  18891  divccncf  18924  causs  19239  lmclim  19243  bcthlem1  19265  ovolfsf  19356  ioombl  19447  iccvolcl  19449  ioorcl  19457  volcn  19486  itg2itg1  19616  dvexp  19827  dvmptfsum  19847  dvexp3  19850  dvef  19852  dvlip  19865  c1lip1  19869  ftc1a  19909  tdeglem1  19969  tdeglem3  19970  tdeglem4  19971  coe1termlem  20164  plyremlem  20209  ptolemy  20392  cos11  20423  logeftb  20466  logleb  20486  logdivlt  20504  logdivle  20505  angval  20631  isppw2  20886  issqf  20907  vmasum  20988  lgsquadlem3  21128  ostth  21321  nb3graprlem2  21449  isspthonpth  21572  wlkdvspthlem  21595  3v3e3cycl1  21619  constr3trllem2  21626  constr3trllem3  21627  eupatrl  21678  ablomul  21931  isdivrngo  22007  vcz  22037  isvc  22048  isnv  22079  isnvi  22080  nmooge0  22256  nmblolbii  22288  blocnilem  22293  ipblnfi  22345  hvpncan2  22530  hvaddsub4  22568  hire  22584  abshicom  22591  hial2eq2  22597  orthcom  22598  hhssabloi  22750  ocsh  22773  shscli  22807  shscom  22809  shsel2  22812  spanss  22838  shjcom  22848  shmodsi  22879  chpsscon3  22993  spansni  23047  spansnmul  23054  spansncol  23058  spanunsni  23069  cmcm2  23106  cm2j  23110  spansncvi  23142  5oalem2  23145  3oalem2  23153  honegsubdi2  23302  adjsym  23324  cnvadj  23383  brafn  23438  kbpj  23447  riesz3i  23553  cnlnadjlem2  23559  cnlnadjlem9  23566  nmopcoi  23586  cnvbraval  23601  leop  23614  leop3  23616  leopmul2i  23626  leoptri  23627  hstrlem3a  23751  cvcon3  23775  cvnsym  23781  mdbr2  23787  dmdmd  23791  dmdbr2  23794  dmdbr3  23796  dmdbr4  23797  dmdbr5  23799  mdsl0  23801  ssmd2  23803  mdslmd1lem1  23816  mdslmd1lem2  23817  mdslmd3i  23823  mdslmd4i  23824  atcveq0  23839  superpos  23845  atnemeq0  23868  atssma  23869  atexch  23872  atomli  23873  atcvatlem  23876  atcvati  23877  chirredlem1  23881  chirredlem3  23883  chirredi  23885  atcvat3i  23887  atdmd  23889  mdsymlem1  23894  mdsymlem3  23896  mdsymlem4  23897  mdsymlem5  23898  mdsymlem8  23901  dmdsym  23904  atdmd2  23905  sumdmdlem  23909  cdjreui  23923  cdj3lem2b  23928  cdj3i  23932  imadifxp  24026  abfmpel  24055  xaddeq0  24107  xrofsup  24114  xeqlelt  24127  xdivpnfrp  24167  xrsinvgval  24187  xrsmulgzz  24188  cnvordtrestixx  24299  indval  24399  esumpfinvallem  24452  sigagenss  24520  brae  24580  dya2iocival  24611  dya2iocnei  24620  dya2iocuni  24621  derangenlem  24845  subfacval2  24861  kur14  24890  elfzp1b  25104  lediv2aALT  25105  mulsuble0b  25181  ntrivcvgfvn0  25216  prodmo  25251  zprod  25252  prodss  25262  fprodcnv  25296  faclim2  25356  funpsstri  25376  setlikespec  25442  dftrpred3g  25491  soseq  25509  wfr3g  25510  wfrlem5  25515  wfrlem10  25520  frrlem5  25540  elno  25555  sltsolem1  25577  nodenselem4  25593  nofulllem5  25615  brbtwn2  25792  colinearalglem4  25796  ax5seglem1  25815  ax5seglem2  25816  axcontlem2  25852  axcontlem12  25862  bpolysum  26047  bpoly4  26053  hfelhf  26070  onsuct0  26139  nndivsub  26155  ltflcei  26187  leceifl  26188  lxflflp1  26189  mblfinlem2  26191  mblfinlem3  26192  ismblfin  26193  ovoliunnfl  26194  voliunnfl  26196  volsupnfl  26197  cnambfre  26201  itg2addnclem2  26203  itg2addnc  26205  itg2gt0cn  26206  elicc3  26257  nn0prpwlem  26262  nn0prpw  26263  isfne  26285  locfincmp  26321  unirep  26351  opelopab3  26355  fvopabf4g  26359  indexa  26372  filbcmb  26379  fzadd2  26382  incsequz2  26390  metf1o  26398  sstotbnd3  26422  isbnd2  26429  bndss  26432  ismtycnv  26448  iccbnd  26486  exidreslem  26489  exidresid  26491  ghomco  26495  isdrngo2  26511  rngoisocnv  26534  riscer  26541  crngohomfo  26553  unichnidl  26578  maxidlmax  26590  igenmin  26611  prtlem16  26655  ismrc  26692  nacsfg  26696  isnacs3  26701  incssnn0  26702  elmapssres  26708  mzpclall  26721  lerabdioph  26802  ltrabdioph  26805  eldioph4b  26809  jm2.17b  26963  congrep  26975  unxpwdom3  27171  islindf  27197  lindff  27200  lindfrn  27206  f1lindf  27207  lnr2i  27235  pmtrfinv  27317  mamudir  27377  matsca2  27389  matbas2  27390  matlmod  27394  expgrowth  27467  2sbc6g  27530  2sbc5g  27531  ordpss  27568  addrcom  27594  fmul01  27624  ioovolcl  27656  stoweidlem34  27697  sigarac  27756  2reu3  27880  afv0nbfvbi  27929  dmfcoafv  27953  ubmelm1fzo  28039  fzonmapblen  28046  ltdifltdiv  28054  swrdltnd  28073  swrdccatin12lem3b  28097  swrdccatin12lem3  28099  swrdccatin12  28101  shwrdidx  28130  shwrdidxmod  28131  shwrdidxm  28134  2shwrd1lem1  28136  2shwrd2lem1  28142  2shwrd2lem2  28143  shwrdeqdif2  28156  shwrdeqrep  28160  shwrd1  28161  shwrdssizelem4a  28169  shwrdssizelem4  28170  frgra3v  28250  frgraregorufr  28300  usg2spot2nb  28312  3impcombi  28783  sspwimp  28884  sspwimpVD  28885  a9e2ndeqALT  28898  iunconlem2  28902  bnj934  29160  paddss1  30453  paddss2  30454  paddss12  30455  pclfinN  30536  erngmul-rN  31450  mapdordlem2  32274
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