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  2243  2eu1  2311  2eu3  2313  eqeqan12rd  2396  sylan9eqr  2434  r19.29_2a  2788  morex  3054  sbcrext  3170  sylan9ssr  3298  pssdifcom1  3649  pssdifcom2  3650  riinn0  4099  breqan12rd  4162  ordelssne  4542  ordtri3or  4547  ordtri2  4550  ordtri4  4552  ordtr2  4559  ordtr3  4560  ordintdif  4564  ordtri2or  4610  dfwe2  4695  ordsucelsuc  4735  ordunisuc2  4757  tfindsg  4773  tfindsg2  4774  dfom2  4780  soinxp  4875  frinxp  4876  seinxp  4877  brelrng  5032  dminss  5219  imainss  5220  funsng  5430  funcnvuni  5451  f1co  5581  f1ocnv  5620  fun11iun  5628  f1oprswap  5650  funimass4  5709  dffv2  5728  fndmdifcom  5767  fsn2  5840  fvtp2  5872  fvtp3  5873  fvtp2g  5875  fvtp3g  5876  cofunex2g  5892  soisoi  5980  oveqan12rd  6033  curry2  6373  soxp  6388  mpt2xopoveqd  6401  tposoprab  6444  brrpssg  6453  sorpsscmpl  6462  smores3  6544  smores2  6545  smoel  6551  tfr3  6589  tz7.48-2  6628  tz7.49  6631  oaordi  6718  oaword  6721  oaord1  6723  oaword2  6725  oa00  6731  oalimcl  6732  oaass  6733  oarec  6734  oacomf1o  6737  omord2  6739  omcan  6741  omword  6742  omword1  6745  omword2  6746  odi  6751  omass  6752  oneo  6753  oen0  6758  oecan  6761  oelim2  6767  nnarcl  6788  nnaordi  6790  nnaordr  6792  nnawordi  6793  nnmsucr  6797  nnmcom  6798  nnaword  6799  nnmordi  6803  nnaordex  6810  oaabslem  6815  omabslem  6818  nnneo  6823  omsmo  6826  ersym  6846  elecg  6872  riiner  6906  ecopovsym  6935  ecovcom  6944  mapvalg  6957  pmvalg  6958  elpmg  6961  pmss12g  6969  ixpconstg  7000  ener  7083  domtr  7089  f1imaeng  7096  fundmen  7109  xpcomco  7127  xpsnen2g  7130  xpdom2  7132  xpdom1g  7134  omxpen  7139  omf1o  7140  enen2  7177  domen2  7179  sdomen2  7181  domtriord  7182  sdomel  7183  onsdominel  7185  infensuc  7214  onomeneq  7225  nndomo  7229  pssnn  7256  unbnn  7292  infcntss  7309  fiint  7312  mapfi  7331  fiin  7355  fiss  7357  oiiso  7432  unwdomg  7478  suc11reg  7500  inf3lem5  7513  infeq5  7518  cantnfp1lem3  7562  r1tr  7628  r1val1  7638  rankr1ai  7650  rankonidlem  7680  onssr1  7683  tskwe  7763  carddom2  7790  carden2  7800  domtri2  7802  cardval2  7804  fidomtri  7806  fidomtri2  7807  harval2  7810  dif1card  7818  infxpenlem  7821  ac5num  7843  alephord3  7885  alephdom  7888  aleph11  7891  alephdom2  7894  cardaleph  7896  dfac3  7928  dfac5  7935  cdacomen  7987  onacda  8003  pwsdompw  8010  ackbij1lem11  8036  ackbij2  8049  cfeq0  8062  cfsuc  8063  cff1  8064  cflim2  8069  cfsmolem  8076  coftr  8079  sornom  8083  infpssrlem4  8112  ssfin4  8116  ssfin2  8126  ssfin3ds  8136  fin23lem31  8149  isf32lem9  8167  hsmexlem5  8236  axdc3lem  8256  axdc3lem2  8257  axdc3lem4  8259  zorn2lem6  8307  brdom3  8332  brdom7disj  8335  brdom6disj  8336  alephval2  8373  alephreg  8383  wuncss  8546  gruen  8613  addcompi  8697  mulcompi  8699  ltapi  8706  ltmpi  8707  nqereu  8732  addcompq  8753  addcomnq  8754  mulcompq  8755  mulcomnq  8756  ltsonq  8772  ltanq  8774  ltmnq  8775  genpnnp  8808  addcompr  8824  mulcompr  8826  ltsopr  8835  ltexprlem2  8840  prlem936  8850  suplem2pr  8856  map2psrpr  8911  axpre-ltadd  8968  xrltnle  9070  axlttri  9073  axsup  9077  ltnle  9081  letri3  9086  leloe  9087  eqlelt  9088  letric  9100  mul31  9159  subcl  9230  pncan2  9237  pncan3  9238  npcan  9239  addsubeq4  9245  npncan3  9264  negsubdi2  9285  muladd  9391  subdi  9392  mulneg2  9396  mulsub  9401  ltleadd  9436  ltsubpos  9445  posdif  9446  addge01  9463  lesub0  9469  wloglei  9484  prodgt02  9781  prodge02  9783  ltdivmul  9807  ledivmul  9808  lt2mul2div  9811  lerec  9817  lt2msq  9819  ltdiv23  9826  lediv23  9827  lediv2a  9829  le2msq  9835  msq11  9836  fimaxre  9880  lbreu  9883  infm3  9892  dfinfmr  9910  creur  9919  creui  9920  cju  9921  nnmulcl  9948  nndivtr  9966  avgle1  10132  avgle2  10133  avgle  10134  nn0nnaddcl  10177  zrevaddcl  10246  znnsub  10247  znn0sub  10248  zextlt  10269  gtndiv  10272  prime  10275  uztrn2  10428  uztric  10432  uz11  10433  uzwo  10464  uzwoOLD  10465  zmax  10496  zbtwnre  10497  rebtwnz  10498  qrevaddcl  10521  rpnnen1lem1  10525  rpnnen1lem2  10526  rpnnen1lem3  10527  rpnnen1lem5  10529  difrp  10570  xrltnsym  10655  xrlttri  10657  xrleloe  10662  xrletri  10669  xrletri3  10670  xrmaxeq  10692  xrmineq  10693  xrmaxlt  10694  xrmaxle  10696  z2ge  10709  qbtwnre  10710  qextlt  10714  qextle  10715  xleneg  10729  xaddcom  10749  xmulcom  10770  xmulneg2  10774  xmulgt0  10787  xrsupsslem  10810  xrinfmsslem  10811  supxrunb1  10823  supxrunb2  10824  ixxssixx  10855  ixxin  10858  ioon0  10867  iccid  10886  iooshf  10914  iccsupr  10922  iooneg  10942  iccneg  10943  iccsplit  10954  fzen  10997  fzass4  11015  fzrev  11032  fznn  11038  elfzm1b  11048  fzm1  11050  fzon  11081  fllt  11135  flbi  11143  flbi2  11144  flzadd  11148  modcyc2  11197  om2uzlt2i  11211  om2uzf1oi  11213  fseqsupubi  11237  expcllem  11312  faclbnd5  11509  hashbnd  11544  hasheni  11552  hasheqf1oi  11555  hashf1rn  11556  hashdom  11573  hashfacen  11623  ccatass  11670  ccatco  11724  shftlem  11803  shftuz  11804  shftfval  11805  shftval4  11812  shftval5  11813  2shfti  11815  seqshft  11820  mulre  11846  sqrlt  11987  abs3dif  12055  abs2difabs  12058  uzin2  12068  rexanre  12070  caubnd  12082  climshftlem  12288  rlimcn2  12304  fsumcnv  12477  geo2lim  12572  efle  12639  reef11  12640  demoivre  12721  demoivreALT  12722  sqr2irr  12768  0dvds  12790  muldvds1  12794  muldvds2  12795  dvdscmulr  12798  dvdssubr  12811  dvdsadd2b  12812  odd2np1  12828  divalglem9  12841  ndvdssub  12847  gcdcllem1  12931  gcdcom  12940  neggcd  12947  gcdabs2  12955  modgcd  12956  dvdsprm  13019  coprmdvds  13022  qredeq  13026  odzdvds  13101  coprimeprodsq  13103  pythagtriplem1  13110  pythagtriplem4  13113  pc2dvds  13172  pc11  13173  pcz  13174  pcprod  13184  prmunb  13202  1arithlem3  13213  1arith  13215  ressabs  13447  acsfn2  13808  issect  13899  pospo  14350  clatglbss  14474  pospropd  14481  pslem  14558  tsrss  14575  spweu  14579  issubmnd  14644  submcl  14673  resmhm2b  14681  frmdmnd  14724  frmd0  14725  grpinvsub  14791  gimcnv  14974  gimco  14975  gictr  14982  cntz2ss  15051  cntzrec  15052  dfod2  15120  lsmcom2  15209  efgred  15300  divsabl  15400  cygabl  15420  eldprd  15482  dfrhm2  15741  lmimcnv  16059  psrbagsuppfi  16485  cnfldexp  16650  cnsrng  16651  xrsdsreval  16659  dvdsrz  16683  znf1o  16748  ocvocv  16814  ocvin  16817  eltg  16938  eltg2  16939  tgss  16949  tgss2  16968  basgen2  16970  bastop1  16974  cldmre  17058  toponmre  17073  opnneiss  17098  restcldr  17153  restfpw  17158  restcls  17160  restntr  17161  ordtbaslem  17167  ordtrest2lem  17182  leordtvallem2  17190  leordtval  17192  cnrest  17264  t0sep  17303  cmpcov  17367  cmpsublem  17377  cmpsub  17378  2ndcomap  17435  ptval  17516  xkoval  17533  txss12  17551  ptrescn  17585  xkopt  17601  hmeofval  17704  txswaphmeolem  17750  txswaphmeo  17751  trfbas2  17789  trfbas  17790  uzrest  17843  numufl  17861  ssufl  17864  flimclsi  17924  hauspwpwf1  17933  ghmcnp  18058  blpnfctr  18349  metequiv  18422  metcnp3  18453  elbl4  18476  restmetu  18482  tngngp  18559  qtopbaslem  18656  bl2ioo  18687  ioo2bl  18688  ioo2blex  18689  xrsxmet  18704  divccn  18767  divccncf  18800  causs  19115  lmclim  19119  bcthlem1  19139  ovolfsf  19228  ioombl  19319  iccvolcl  19321  ioorcl  19329  volcn  19358  itg2itg1  19488  dvexp  19699  dvmptfsum  19719  dvexp3  19722  dvef  19724  dvlip  19737  c1lip1  19741  ftc1a  19781  tdeglem1  19841  tdeglem3  19842  tdeglem4  19843  coe1termlem  20036  plyremlem  20081  ptolemy  20264  cos11  20295  logeftb  20338  logleb  20358  logdivlt  20376  logdivle  20377  angval  20503  isppw2  20758  issqf  20779  vmasum  20860  lgsquadlem3  21000  ostth  21193  nb3graprlem2  21320  wlkdvspthlem  21448  3v3e3cycl1  21472  constr3trllem2  21479  constr3trllem3  21480  eupatrl  21531  ablomul  21784  isdivrngo  21860  vcz  21890  isvc  21901  isnv  21932  isnvi  21933  nmooge0  22109  nmblolbii  22141  blocnilem  22146  ipblnfi  22198  hvpncan2  22383  hvaddsub4  22421  hire  22437  abshicom  22444  hial2eq2  22450  orthcom  22451  hhssabloi  22603  ocsh  22626  shscli  22660  shscom  22662  shsel2  22665  spanss  22691  shjcom  22701  shmodsi  22732  chpsscon3  22846  spansni  22900  spansnmul  22907  spansncol  22911  spanunsni  22922  cmcm2  22959  cm2j  22963  spansncvi  22995  5oalem2  22998  3oalem2  23006  honegsubdi2  23155  adjsym  23177  cnvadj  23236  brafn  23291  kbpj  23300  riesz3i  23406  cnlnadjlem2  23412  cnlnadjlem9  23419  nmopcoi  23439  cnvbraval  23454  leop  23467  leop3  23469  leopmul2i  23479  leoptri  23480  hstrlem3a  23604  cvcon3  23628  cvnsym  23634  mdbr2  23640  dmdmd  23644  dmdbr2  23647  dmdbr3  23649  dmdbr4  23650  dmdbr5  23652  mdsl0  23654  ssmd2  23656  mdslmd1lem1  23669  mdslmd1lem2  23670  mdslmd3i  23676  mdslmd4i  23677  atcveq0  23692  superpos  23698  atnemeq0  23721  atssma  23722  atexch  23725  atomli  23726  atcvatlem  23729  atcvati  23730  chirredlem1  23734  chirredlem3  23736  chirredi  23738  atcvat3i  23740  atdmd  23742  mdsymlem1  23747  mdsymlem3  23749  mdsymlem4  23750  mdsymlem5  23751  mdsymlem8  23754  dmdsym  23757  atdmd2  23758  sumdmdlem  23762  cdjreui  23776  cdj3lem2b  23781  cdj3i  23785  imadifxp  23874  abfmpel  23902  xrofsup  23955  xeqlelt  23968  xdivpnfrp  24011  xaddeq0  24023  xrsinvgval  24025  xrsmulgzz  24026  cnvordtrestixx  24108  indval  24200  esumpfinvallem  24253  sigagenss  24321  brae  24379  dya2iocival  24410  dya2iocnei  24419  dya2iocuni  24420  derangenlem  24629  subfacval2  24645  kur14  24674  elfzp1b  24888  lediv2aALT  24889  mulsuble0b  24965  ntrivcvgfvn0  24999  prodmo  25034  zprod  25035  prodss  25045  faclim2  25118  funpsstri  25138  setlikespec  25204  dftrpred3g  25253  soseq  25271  wfr3g  25272  wfrlem5  25277  wfrlem10  25282  frrlem5  25302  elno  25317  sltsolem1  25339  nodenselem4  25355  nofulllem5  25377  brbtwn2  25551  colinearalglem4  25555  ax5seglem1  25574  ax5seglem2  25575  axcontlem2  25611  axcontlem12  25621  bpolysum  25806  bpoly4  25812  hfelhf  25829  onsuct0  25898  nndivsub  25914  ltflcei  25943  leceifl  25944  lxflflp1  25945  ovoliunnfl  25946  voliunnfl  25948  volsupnfl  25949  itg2addnclem2  25951  itg2gt0cn  25953  elicc3  26004  nn0prpwlem  26009  nn0prpw  26010  isfne  26032  locfincmp  26068  unirep  26098  opelopab3  26102  fvopabf4g  26106  indexa  26119  filbcmb  26126  fzadd2  26129  incsequz2  26137  metf1o  26145  sstotbnd3  26169  isbnd2  26176  bndss  26179  ismtycnv  26195  iccbnd  26233  exidreslem  26236  exidresid  26238  ghomco  26242  isdrngo2  26258  rngoisocnv  26281  riscer  26288  crngohomfo  26300  unichnidl  26325  maxidlmax  26337  igenmin  26358  prtlem16  26402  ismrc  26439  nacsfg  26443  isnacs3  26448  incssnn0  26449  elmapssres  26455  mzpclall  26468  lerabdioph  26549  ltrabdioph  26552  eldioph4b  26556  jm2.17b  26710  congrep  26722  unxpwdom3  26918  islindf  26944  lindff  26947  lindfrn  26953  f1lindf  26954  lnr2i  26982  pmtrfinv  27064  mamudir  27124  matsca2  27136  matbas2  27137  matlmod  27141  expgrowth  27214  2sbc6g  27277  2sbc5g  27278  ordpss  27315  addrcom  27341  fmul01  27371  ioovolcl  27403  stoweidlem34  27444  sigarac  27503  2reu3  27627  afv0nbfvbi  27677  dmfcoafv  27701  frgra3v  27748  frgraregorufr  27798  3impcombi  28263  sspwimp  28364  sspwimpVD  28365  a9e2ndeqALT  28378  bnj934  28637  paddss1  29982  paddss2  29983  paddss12  29984  pclfinN  30065  erngmul-rN  30979  mapdordlem2  31803
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