MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adantlr Unicode version

Theorem adantlr 695
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypothesis
Ref Expression
adant2.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
adantlr  |-  ( ( ( ph  /\  th )  /\  ps )  ->  ch )

Proof of Theorem adantlr
StepHypRef Expression
1 simpl 443 . 2  |-  ( (
ph  /\  th )  ->  ph )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan 457 1  |-  ( ( ( ph  /\  th )  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  ad2antrr  706  ad2ant2r  727  ad2ant2rl  729  pm2.61ddan  767  pm2.61dda  768  3ad2antl1  1117  3ad2antl2  1118  3adant1r  1175  ax11eq  2132  ax11el  2133  ax11indalem  2136  ax11inda2ALT  2137  nfeud2  2155  pm2.61da2ne  2525  pm2.61da3ne  2526  uneqdifeq  3542  intab  3892  pofun  4330  tz7.7  4418  ordtr3  4437  ralxfrd  4548  onmindif2  4603  peano5  4679  poinxp  4753  relop  4834  soex  5122  fun11iun  5493  ssimaex  5584  fndmdif  5629  iinpreima  5655  fconst2g  5728  foeqcnvco  5804  f1eqcocnv  5805  isocnv  5827  grprinvd  6059  grpridd  6060  caofdi  6113  caofdir  6114  frxp  6225  riota2df  6325  riotasvdOLD  6348  riotasv2d  6349  tfrlem2  6392  oaordi  6544  oawordri  6548  oaass  6559  omlimcl  6576  odi  6577  omass  6578  oeordi  6585  oewordri  6590  oeoe  6597  nnaordi  6616  nnawordex  6635  nnaordex  6636  omsmolem  6651  omsmo  6652  xpdom2  6957  sbthlem9  6979  mapdom2  7032  ordunifi  7107  fiint  7133  fodomfib  7136  ordiso2  7230  unwdomg  7298  noinfepOLD  7361  cantnflem1c  7389  cantnflem1  7391  fidomtri  7626  dfac5  7755  dfac9  7762  ackbij2lem3  7867  cff1  7884  cfsmolem  7896  cfcoflem  7898  infpssrlem4  7932  fin23lem11  7943  fin23lem26  7951  fin23lem39  7976  axcc3  8064  axdc3lem2  8077  axdc3lem4  8079  zorn2lem6  8128  zorn2lem7  8129  fpwwe2lem10  8261  fpwwe2lem11  8262  fpwwe2lem12  8263  fpwwe2lem13  8264  fpwwe2  8265  intwun  8357  eltsk2g  8373  inatsk  8400  tskord  8402  r1tskina  8404  tskuni  8405  gruwun  8435  intgru  8436  grutsk1  8443  addcanpi  8523  mulcanpi  8524  indpi  8531  genpnmax  8631  addclprlem2  8641  mulclprlem  8643  supsrlem  8733  axpre-sup  8791  1re  8837  axsup  8898  00id  8987  addsubeq4  9066  divcan6  9467  ltmul12a  9612  lemul12b  9613  ledivdiv  9645  lediv12a  9649  lbinfm  9707  supmul1  9719  supmul  9722  nn2ge  9771  zrevaddcl  10063  zextle  10085  suprzcl  10091  fzind  10110  uz11  10250  uzwo3  10311  zbtwnre  10314  qreccl  10336  qrevaddcl  10338  irradd  10340  rpnnen1lem5  10346  xrlttr  10474  xaddass  10569  xleadd1a  10573  xlt2add  10580  xmulneg1  10589  xmulgt0  10603  xmulge0  10604  xmulasslem3  10606  xlemul1a  10608  xadddilem  10614  xrsupsslem  10625  xrinfmsslem  10626  xrub  10630  supxrun  10634  supxrunb1  10638  supxrbnd  10647  ixxin  10673  iccsplit  10768  iccshftr  10769  iccshftl  10771  iccdil  10773  icccntr  10775  fzaddel  10826  fzrev  10846  modadd1  11001  modmul1  11002  seqf2  11065  seqfeq2  11069  seqfeq  11071  sermono  11078  seqsplit  11079  seqcaopr2  11082  seqf1olem2a  11084  seqf1olem2  11086  seqid  11091  seqhomo  11093  seqz  11094  seqfeq3  11096  seqof  11103  expcllem  11114  mulexp  11141  expadd  11144  expaddz  11146  expmulz  11148  expdiv  11152  leexp1a  11160  expnlbnd  11231  bcpasc  11333  bccl  11334  hashdom  11361  hashfacen  11392  seqcoll  11401  revco  11489  cnpart  11725  sqrdiv  11751  lo1bdd2  11998  lo1bddrp  11999  lo1o1  12006  o1lo1  12011  o1lo12  12012  climrlim2  12021  rlimuni  12024  climshftlem  12048  rlimcld2  12052  rlimcn2  12064  climcn1  12065  rlimo1  12090  lo1add  12100  lo1mul  12101  climsqz  12114  climsqz2  12115  rlimsqzlem  12122  lo1le  12125  rlimno1  12127  clim2ser  12128  clim2ser2  12129  isermulc2  12131  climub  12135  isercolllem3  12140  serf0  12153  iseraltlem1  12154  iseralt  12157  sumeq2ii  12166  fsumcvg  12185  sumrb  12186  fsumf1o  12196  sumss  12197  fsumss  12198  fsumcvg3  12202  fsumcl2lem  12204  fsumcllem  12205  fsumadd  12211  fsumrev2  12244  fsum2mul  12251  fsum00  12256  fsumtscopo  12260  fsumparts  12264  fsumrlim  12269  fsumo1  12270  o1fsum  12271  iserabs  12273  isumsup2  12305  isumltss  12307  climcnds  12310  geomulcvg  12332  geoisum  12333  mertenslem1  12340  mertenslem2  12341  mertens  12342  eftlcvg  12386  rpnnen2lem5  12497  negdvdsb  12545  dvdsnegb  12546  fsumdvds  12572  dvdsext  12579  gcdcllem3  12692  dvdssq  12739  eucalgf  12753  phiprmpw  12844  eulerthlem2  12850  pc2dvds  12931  prmpwdvds  12951  prmreclem5  12967  prmreclem6  12968  1arith  12974  vdwlem6  13033  vdwnnlem3  13044  ramlb  13066  mreexmrid  13545  mreexexlem4d  13549  isacs2  13555  mreacs  13560  issubc  13712  funcres2b  13771  natpropd  13850  lubid  14116  poslubmo  14250  isacs4lem  14271  isacs5lem  14272  spwpr4  14340  mndpropd  14398  prdsidlem  14404  prdsmndd  14405  mhmpropd  14421  0mhm  14435  resmhm2  14437  resmhm2b  14438  pwsdiagmhm  14445  grplcan  14534  mulgnndir  14589  mulgnn0dir  14590  issubg2  14636  issubg4  14638  subgint  14641  ghmf1  14711  subgga  14754  gasubg  14756  cntzsubm  14811  odf1  14875  dfod2  14877  sylow1lem2  14910  sylow1lem3  14911  sylow3lem1  14938  frgpuplem  15081  frgpup1  15084  divsabl  15157  cyggenod  15171  cyggex2  15183  gsumval3  15191  gsumzaddlem  15203  prdsgsum  15229  dmdprd  15236  dprdfcntz  15250  dprdfeq0  15257  dprdlub  15261  dmdprdsplitlem  15272  dprd2da  15277  ablfac1c  15306  ablfac1eu  15308  rnglghm  15388  rngrghm  15389  gsumdixp  15392  irrednegb  15493  drngmul0or  15533  drngpropd  15539  issubrg2  15565  subrgint  15567  abvneg  15599  lmodvsghm  15686  lmodprop2d  15687  islss3  15716  lssintcl  15721  prdslmodd  15726  pwslmod  15727  pwsdiaglmhm  15814  lmhmpropd  15826  lvecvs0or  15861  lbsextlem2  15912  divsrhm  15989  unitrrg  16034  mplsubglem  16179  mplmonmul  16208  mplcoe1  16209  mplcoe2  16211  coe1tmmul  16353  cygznlem3  16523  ocvlss  16572  elcls  16810  opnssneib  16852  neissex  16864  maxlp  16878  tgrest  16890  restcld  16903  perfopn  16915  leordtval  16943  iscnp3  16974  cnpnei  16993  cnrest  17013  restcnrm  17090  lpcls  17092  llycmpkgen2  17245  1stckgenlem  17248  ptbasfi  17276  tx1cn  17303  xkoccn  17313  txcnp  17314  ptcnplem  17315  ptcn  17321  ptrescn  17333  kqt0lem  17427  isr0  17428  regr1lem2  17431  ptunhmeo  17499  trfbas2  17538  trfil2  17582  ufileu  17614  elfm3  17645  rnelfmlem  17647  cnflf  17697  fclsopn  17709  ufilcmp  17727  cnfcf  17737  alexsublem  17738  alexsub  17739  alexsubALTlem3  17743  alexsubALTlem4  17744  ptcmplem3  17748  ptcmplem5  17750  tmdmulg  17775  tgpmulg  17776  ghmcnp  17797  tsmsxplem1  17835  prdsxmetlem  17932  elbl3  17951  blin  17970  blssex  17973  blpnfctr  17982  prdsbl  18037  mopni2  18039  blsscls2  18050  metss  18054  stdbdmet  18062  metrest  18070  metcn  18089  txmetcn  18094  ngplcan  18132  isngp4  18133  ngppropd  18153  tngnm  18167  nmoid  18251  bl2ioo  18298  blcvx  18304  xrsxmet  18315  iocopnst  18438  icccvx  18448  evth2  18458  lebnumlem1  18459  pcoass  18522  pi1xfr  18553  pi1coghm  18559  nmoleub2lem  18595  tchcph  18667  lmmbr  18684  lmnn  18689  iscau2  18703  causs  18724  equivcfil  18725  lmle  18727  bcthlem4  18749  bcth2  18752  minveclem4  18796  ivthle  18816  ivthle2  18817  ovollb2lem  18847  ovoliunlem2  18862  ovolshftlem1  18868  ovolscalem1  18872  ovolicc2lem4  18879  ovolicc2lem5  18880  ioombl1lem4  18918  uniioombllem3  18940  uniioombllem4  18941  uniioombllem6  18943  dyaddisjlem  18950  vitalilem4  18966  ismbf  18985  mbfposb  19008  mbfsup  19019  mbfinf  19020  mbflimsup  19021  i1fd  19036  itg1val2  19039  itg1ge0  19041  itg1addlem4  19054  itg1addlem5  19055  i1fmulclem  19057  itg1mulc  19059  i1fres  19060  itg1climres  19069  mbfi1fseqlem4  19073  mbfi1flimlem  19077  mbfmullem2  19079  itg2seq  19097  itg2lea  19099  itg2splitlem  19103  itg2split  19104  itg2monolem1  19105  itg2monolem3  19107  itg2mono  19108  itg2i1fseqle  19109  itg2gt0  19115  itg2cnlem1  19116  itg2cn  19118  iblitg  19123  itgss  19166  itgeqa  19168  itgfsum  19181  iblabsr  19184  iblmulc2  19185  itgsplit  19190  itgsplitioo  19192  itgcn  19197  ditgsplitlem  19210  ditgsplit  19211  limciun  19244  dvcj  19299  dvfre  19300  dvlip  19340  lhop1lem  19360  lhop  19363  dvfsumle  19368  dvfsumge  19369  dvfsumabs  19370  dvfsumlem3  19375  dvfsumrlim  19378  dvfsumrlim2  19379  dvfsumrlim3  19380  ftc1lem1  19382  ftc1a  19384  ftc1lem4  19386  itgsubstlem  19395  evlslem1  19399  mpfind  19428  deg1leb  19481  elplyd  19584  plyeq0lem  19592  plypf1  19594  plyaddlem1  19595  plymullem1  19596  coeeulem  19606  plyco  19623  coeeq2  19624  dgrcolem1  19654  plydivlem2  19674  plydivlem4  19676  plydivex  19677  elqaalem2  19700  taylfvallem1  19736  dvtaylp  19749  mtest  19781  itgulm  19784  psergf  19788  pserulm  19798  psercn2  19799  pserdvlem2  19804  abelthlem8  19815  abelthlem9  19816  abssinper  19886  tanord  19900  advlogexp  20002  logtayllem  20006  logtayl  20007  cxpmul2z  20038  abscxp2  20040  angpined  20127  rlimcnp  20260  xrlimcnp  20263  efrlim  20264  rlimcxp  20268  emcllem7  20295  fsumharmonic  20305  wilthlem2  20307  ftalem1  20310  mumul  20419  fsumdvdsmul  20435  ppiub  20443  fsumvma  20452  dchrelbasd  20478  dchrsum2  20507  lgsval2lem  20545  lgsdir2  20567  lgsne0  20572  lgsquadlem1  20593  rpvmasumlem  20636  dchrisumlem2  20639  dchrisumlem3  20640  dchrisum  20641  dchrvmasumiflem1  20650  rpvmasum2  20661  dchrisum0re  20662  mudivsum  20679  mulogsum  20681  mulog2sumlem2  20684  pntrsumbnd  20715  pntrlog2bnd  20733  pntpbnd1  20735  pntlemj  20752  pntlemf  20754  abvcxp  20764  padicabv  20779  padicabvcxp  20781  grpoidinvlem3  20873  grpolcan  20900  isgrp2d  20902  ghsubgolem  21037  nvmul0or  21210  nvelbl  21262  nvelbl2  21263  sspmval  21309  sspival  21314  sspimsval  21316  nmoub3i  21351  blocnilem  21382  sspph  21433  ubthlem1  21449  ubthlem3  21451  minvecolem3  21455  hvmul0or  21604  hvaddsub4  21657  shsel3  21894  shsel1  21900  spansncol  22147  chscllem2  22217  5oalem2  22234  5oalem4  22236  3oalem2  22242  hoaddcl  22338  eigposi  22416  nmopub2tALT  22489  unoplin  22500  nmfnleub2  22506  hmopadj2  22521  hmoplin  22522  kbpj  22536  eighmorth  22544  0cnop  22559  0cnfn  22560  lnconi  22613  nlelchi  22641  riesz3i  22642  cnlnadjlem6  22652  adjadd  22673  branmfn  22685  bra11  22688  leop2  22704  leopadd  22712  leopmuli  22713  leoptri  22716  leopnmid  22718  nmopleid  22719  opsqrlem1  22720  hmopidmchi  22731  pjss2coi  22744  pjssdif1i  22755  pj3si  22787  pj3cor1i  22789  hstle  22810  hstrlem3a  22840  cvcon3  22864  mdbr2  22876  dmdbr2  22883  mddmd2  22889  mdslmd2i  22910  csmdsymi  22914  superpos  22934  atordi  22964  atcvatlem  22965  chirredlem1  22970  chirredi  22974  mdsymlem1  22983  mdsymlem2  22984  mdsymlem3  22985  mdsymlem4  22986  mdsymlem5  22987  sumdmdii  22995  cdj3i  23021  ballotlemic  23065  ballotlem1c  23066  ballotlemsv  23068  ballotlemsima  23074  opfv  23190  xppreima  23211  xrmulc1cn  23303  rge0scvg  23373  lmxrge0  23375  lmdvg  23376  gsumpropd2lem  23379  hashge1  23388  esumpr2  23439  esumpcvgval  23446  esumcvg  23454  measdivcstOLD  23551  measdivcst  23552  subfacp1lem5  23715  divelunit  24080  dedekind  24082  fundmpss  24122  dfon2lem8  24146  poseq  24253  soseq  24254  wfrlem4  24259  frrlem4  24284  sltval2  24310  nocvxminlem  24344  nobndup  24354  nobnddown  24355  brcgr  24528  eqeelen  24532  brbtwn2  24533  colinearalglem4  24537  colinearalg  24538  axcgrid  24544  axsegconlem3  24547  axcontlem2  24593  axcontlem8  24599  hfext  24813  areacirclem4  24927  areacirclem6  24930  npincppr  25159  cbicp  25166  toplat  25290  trran2  25393  ltrran2  25403  ltrinvlem  25406  usptoplem  25546  istopx  25547  prcnt  25551  addidv2  25657  imonclem  25813  elicc3  26228  opnregcld  26248  filnetlem4  26330  eqfnun  26387  upixp  26403  indexdom  26413  fipreimaOLD  26415  filbcmb  26432  fzadd2  26444  sdclem1  26453  fdc  26455  fdc1  26456  incsequz  26458  nnubfi  26460  nninfnub  26461  csbrn  26462  metf1o  26469  geomcau  26475  sstotbnd2  26498  equivtotbnd  26502  isbnd3b  26509  bndss  26510  equivbnd  26514  equivbnd2  26516  prdsbnd  26517  prdstotbnd  26518  prdsbnd2  26519  cntotbnd  26520  ismtycnv  26526  heibor1  26534  heiborlem1  26535  bfplem2  26547  bfp  26548  rrnmet  26553  rrndstprj1  26554  rrncmslem  26556  rrnequiv  26559  ghomco  26573  grpokerinj  26575  isdrngo2  26589  rngohomco  26605  riscer  26619  idlsubcl  26648  keridl  26657  ispridl2  26663  igenval2  26691  isfldidl  26693  ispridlc  26695  pridlc3  26698  dmncan1  26701  isnacs3  26785  mzpexpmpt  26823  mzpindd  26824  mzpmfp  26825  rexzrexnn0  26885  fphpdo  26900  ctbnfien  26901  pellexlem5  26918  monotoddzzfi  27027  rmxnn  27038  setindtr  27117  pw2f1ocnv  27130  fnwe2  27150  kelac1  27161  dfac21  27164  islssfg2  27169  filnm  27192  dsmmsubg  27209  dsmmlss  27210  frlmup1  27250  isnumbasgrplem3  27270  lindff1  27290  islindf3  27296  rngunsnply  27378  f1otrspeq  27390  symggen  27411  psgnunilem2  27418  mndvass  27447  mndvlid  27448  mndvrid  27449  grpvlinv  27450  mamudi  27461  cncmpmax  27703  refsum2cnlem1  27708  fmuldfeq  27713  fmul01lt1lem1  27714  fmul01lt1lem2  27715  climinf  27732  climreeq  27739  stoweidlem14  27763  stoweidlem26  27775  stoweidlem27  27776  stoweidlem32  27781  stoweidlem42  27791  stoweidlem48  27797  stoweidlem61  27810  stoweidlem62  27811  stoweid  27812  stirlinglem5  27827  stirlinglem10  27832  uvtxnm1nbgra  28166  bnj605  28939  bnj1137  29025  lshpnelb  29174  lshpset2N  29309  isat3  29497  atnle  29507  islln2a  29706  2at0mat0  29714  pcl0bN  30112  cdlemg1cN  30776  diaglbN  31245  dib1dim2  31358  diclspsn  31384  dihlsscpre  31424  dihmeetALTN  31517  dihglblem6  31530  dochshpncl  31574  mapdval2N  31820  hdmap11lem2  32035
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