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  2134  ax11el  2135  ax11indalem  2138  ax11inda2ALT  2139  nfeud2  2157  pm2.61da2ne  2527  pm2.61da3ne  2528  uneqdifeq  3544  intab  3894  pofun  4332  tz7.7  4420  ordtr3  4439  ralxfrd  4550  onmindif2  4605  peano5  4681  poinxp  4755  relop  4836  soex  5124  fun11iun  5495  ssimaex  5586  fndmdif  5631  iinpreima  5657  fconst2g  5730  foeqcnvco  5806  f1eqcocnv  5807  isocnv  5829  grprinvd  6061  grpridd  6062  caofdi  6115  caofdir  6116  frxp  6227  riota2df  6327  riotasvdOLD  6350  riotasv2d  6351  tfrlem2  6394  oaordi  6546  oawordri  6550  oaass  6561  omlimcl  6578  odi  6579  omass  6580  oeordi  6587  oewordri  6592  oeoe  6599  nnaordi  6618  nnawordex  6637  nnaordex  6638  omsmolem  6653  omsmo  6654  xpdom2  6959  sbthlem9  6981  mapdom2  7034  ordunifi  7109  fiint  7135  fodomfib  7138  ordiso2  7232  unwdomg  7300  noinfepOLD  7363  cantnflem1c  7391  cantnflem1  7393  fidomtri  7628  dfac5  7757  dfac9  7764  ackbij2lem3  7869  cff1  7886  cfsmolem  7898  cfcoflem  7900  infpssrlem4  7934  fin23lem11  7945  fin23lem26  7953  fin23lem39  7978  axcc3  8066  axdc3lem2  8079  axdc3lem4  8081  zorn2lem6  8130  zorn2lem7  8131  fpwwe2lem10  8263  fpwwe2lem11  8264  fpwwe2lem12  8265  fpwwe2lem13  8266  fpwwe2  8267  intwun  8359  eltsk2g  8375  inatsk  8402  tskord  8404  r1tskina  8406  tskuni  8407  gruwun  8437  intgru  8438  grutsk1  8445  addcanpi  8525  mulcanpi  8526  indpi  8533  genpnmax  8633  addclprlem2  8643  mulclprlem  8645  supsrlem  8735  axpre-sup  8793  1re  8839  axsup  8900  00id  8989  addsubeq4  9068  divcan6  9469  ltmul12a  9614  lemul12b  9615  ledivdiv  9647  lediv12a  9651  lbinfm  9709  supmul1  9721  supmul  9724  nn2ge  9773  zrevaddcl  10065  zextle  10087  suprzcl  10093  fzind  10112  uz11  10252  uzwo3  10313  zbtwnre  10316  qreccl  10338  qrevaddcl  10340  irradd  10342  rpnnen1lem5  10348  xrlttr  10476  xaddass  10571  xleadd1a  10575  xlt2add  10582  xmulneg1  10591  xmulgt0  10605  xmulge0  10606  xmulasslem3  10608  xlemul1a  10610  xadddilem  10616  xrsupsslem  10627  xrinfmsslem  10628  xrub  10632  supxrun  10636  supxrunb1  10640  supxrbnd  10649  ixxin  10675  iccsplit  10770  iccshftr  10771  iccshftl  10773  iccdil  10775  icccntr  10777  fzaddel  10828  fzrev  10848  modadd1  11003  modmul1  11004  seqf2  11067  seqfeq2  11071  seqfeq  11073  sermono  11080  seqsplit  11081  seqcaopr2  11084  seqf1olem2a  11086  seqf1olem2  11088  seqid  11093  seqhomo  11095  seqz  11096  seqfeq3  11098  seqof  11105  expcllem  11116  mulexp  11143  expadd  11146  expaddz  11148  expmulz  11150  expdiv  11154  leexp1a  11162  expnlbnd  11233  bcpasc  11335  bccl  11336  hashdom  11363  hashfacen  11394  seqcoll  11403  revco  11491  cnpart  11727  sqrdiv  11753  lo1bdd2  12000  lo1bddrp  12001  lo1o1  12008  o1lo1  12013  o1lo12  12014  climrlim2  12023  rlimuni  12026  climshftlem  12050  rlimcld2  12054  rlimcn2  12066  climcn1  12067  rlimo1  12092  lo1add  12102  lo1mul  12103  climsqz  12116  climsqz2  12117  rlimsqzlem  12124  lo1le  12127  rlimno1  12129  clim2ser  12130  clim2ser2  12131  isermulc2  12133  climub  12137  isercolllem3  12142  serf0  12155  iseraltlem1  12156  iseralt  12159  sumeq2ii  12168  fsumcvg  12187  sumrb  12188  fsumf1o  12198  sumss  12199  fsumss  12200  fsumcvg3  12204  fsumcl2lem  12206  fsumcllem  12207  fsumadd  12213  fsumrev2  12246  fsum2mul  12253  fsum00  12258  fsumtscopo  12262  fsumparts  12266  fsumrlim  12271  fsumo1  12272  o1fsum  12273  iserabs  12275  isumsup2  12307  isumltss  12309  climcnds  12312  geomulcvg  12334  geoisum  12335  mertenslem1  12342  mertenslem2  12343  mertens  12344  eftlcvg  12388  rpnnen2lem5  12499  negdvdsb  12547  dvdsnegb  12548  fsumdvds  12574  dvdsext  12581  gcdcllem3  12694  dvdssq  12741  eucalgf  12755  phiprmpw  12846  eulerthlem2  12852  pc2dvds  12933  prmpwdvds  12953  prmreclem5  12969  prmreclem6  12970  1arith  12976  vdwlem6  13035  vdwnnlem3  13046  ramlb  13068  mreexmrid  13547  mreexexlem4d  13551  isacs2  13557  mreacs  13562  issubc  13714  funcres2b  13773  natpropd  13852  lubid  14118  poslubmo  14252  isacs4lem  14273  isacs5lem  14274  spwpr4  14342  mndpropd  14400  prdsidlem  14406  prdsmndd  14407  mhmpropd  14423  0mhm  14437  resmhm2  14439  resmhm2b  14440  pwsdiagmhm  14447  grplcan  14536  mulgnndir  14591  mulgnn0dir  14592  issubg2  14638  issubg4  14640  subgint  14643  ghmf1  14713  subgga  14756  gasubg  14758  cntzsubm  14813  odf1  14877  dfod2  14879  sylow1lem2  14912  sylow1lem3  14913  sylow3lem1  14940  frgpuplem  15083  frgpup1  15086  divsabl  15159  cyggenod  15173  cyggex2  15185  gsumval3  15193  gsumzaddlem  15205  prdsgsum  15231  dmdprd  15238  dprdfcntz  15252  dprdfeq0  15259  dprdlub  15263  dmdprdsplitlem  15274  dprd2da  15279  ablfac1c  15308  ablfac1eu  15310  rnglghm  15390  rngrghm  15391  gsumdixp  15394  irrednegb  15495  drngmul0or  15535  drngpropd  15541  issubrg2  15567  subrgint  15569  abvneg  15601  lmodvsghm  15688  lmodprop2d  15689  islss3  15718  lssintcl  15723  prdslmodd  15728  pwslmod  15729  pwsdiaglmhm  15816  lmhmpropd  15828  lvecvs0or  15863  lbsextlem2  15914  divsrhm  15991  unitrrg  16036  mplsubglem  16181  mplmonmul  16210  mplcoe1  16211  mplcoe2  16213  coe1tmmul  16355  cygznlem3  16525  ocvlss  16574  elcls  16812  opnssneib  16854  neissex  16866  maxlp  16880  tgrest  16892  restcld  16905  perfopn  16917  leordtval  16945  iscnp3  16976  cnpnei  16995  cnrest  17015  restcnrm  17092  lpcls  17094  llycmpkgen2  17247  1stckgenlem  17250  ptbasfi  17278  tx1cn  17305  xkoccn  17315  txcnp  17316  ptcnplem  17317  ptcn  17323  ptrescn  17335  kqt0lem  17429  isr0  17430  regr1lem2  17433  ptunhmeo  17501  trfbas2  17540  trfil2  17584  ufileu  17616  elfm3  17647  rnelfmlem  17649  cnflf  17699  fclsopn  17711  ufilcmp  17729  cnfcf  17739  alexsublem  17740  alexsub  17741  alexsubALTlem3  17745  alexsubALTlem4  17746  ptcmplem3  17750  ptcmplem5  17752  tmdmulg  17777  tgpmulg  17778  ghmcnp  17799  tsmsxplem1  17837  prdsxmetlem  17934  elbl3  17953  blin  17972  blssex  17975  blpnfctr  17984  prdsbl  18039  mopni2  18041  blsscls2  18052  metss  18056  stdbdmet  18064  metrest  18072  metcn  18091  txmetcn  18096  ngplcan  18134  isngp4  18135  ngppropd  18155  tngnm  18169  nmoid  18253  bl2ioo  18300  blcvx  18306  xrsxmet  18317  iocopnst  18440  icccvx  18450  evth2  18460  lebnumlem1  18461  pcoass  18524  pi1xfr  18555  pi1coghm  18561  nmoleub2lem  18597  tchcph  18669  lmmbr  18686  lmnn  18691  iscau2  18705  causs  18726  equivcfil  18727  lmle  18729  bcthlem4  18751  bcth2  18754  minveclem4  18798  ivthle  18818  ivthle2  18819  ovollb2lem  18849  ovoliunlem2  18864  ovolshftlem1  18870  ovolscalem1  18874  ovolicc2lem4  18881  ovolicc2lem5  18882  ioombl1lem4  18920  uniioombllem3  18942  uniioombllem4  18943  uniioombllem6  18945  dyaddisjlem  18952  vitalilem4  18968  ismbf  18987  mbfposb  19010  mbfsup  19021  mbfinf  19022  mbflimsup  19023  i1fd  19038  itg1val2  19041  itg1ge0  19043  itg1addlem4  19056  itg1addlem5  19057  i1fmulclem  19059  itg1mulc  19061  i1fres  19062  itg1climres  19071  mbfi1fseqlem4  19075  mbfi1flimlem  19079  mbfmullem2  19081  itg2seq  19099  itg2lea  19101  itg2splitlem  19105  itg2split  19106  itg2monolem1  19107  itg2monolem3  19109  itg2mono  19110  itg2i1fseqle  19111  itg2gt0  19117  itg2cnlem1  19118  itg2cn  19120  iblitg  19125  itgss  19168  itgeqa  19170  itgfsum  19183  iblabsr  19186  iblmulc2  19187  itgsplit  19192  itgsplitioo  19194  itgcn  19199  ditgsplitlem  19212  ditgsplit  19213  limciun  19246  dvcj  19301  dvfre  19302  dvlip  19342  lhop1lem  19362  lhop  19365  dvfsumle  19370  dvfsumge  19371  dvfsumabs  19372  dvfsumlem3  19377  dvfsumrlim  19380  dvfsumrlim2  19381  dvfsumrlim3  19382  ftc1lem1  19384  ftc1a  19386  ftc1lem4  19388  itgsubstlem  19397  evlslem1  19401  mpfind  19430  deg1leb  19483  elplyd  19586  plyeq0lem  19594  plypf1  19596  plyaddlem1  19597  plymullem1  19598  coeeulem  19608  plyco  19625  coeeq2  19626  dgrcolem1  19656  plydivlem2  19676  plydivlem4  19678  plydivex  19679  elqaalem2  19702  taylfvallem1  19738  dvtaylp  19751  mtest  19783  itgulm  19786  psergf  19790  pserulm  19800  psercn2  19801  pserdvlem2  19806  abelthlem8  19817  abelthlem9  19818  abssinper  19888  tanord  19902  advlogexp  20004  logtayllem  20008  logtayl  20009  cxpmul2z  20040  abscxp2  20042  angpined  20129  rlimcnp  20262  xrlimcnp  20265  efrlim  20266  rlimcxp  20270  emcllem7  20297  fsumharmonic  20307  wilthlem2  20309  ftalem1  20312  mumul  20421  fsumdvdsmul  20437  ppiub  20445  fsumvma  20454  dchrelbasd  20480  dchrsum2  20509  lgsval2lem  20547  lgsdir2  20569  lgsne0  20574  lgsquadlem1  20595  rpvmasumlem  20638  dchrisumlem2  20641  dchrisumlem3  20642  dchrisum  20643  dchrvmasumiflem1  20652  rpvmasum2  20663  dchrisum0re  20664  mudivsum  20681  mulogsum  20683  mulog2sumlem2  20686  pntrsumbnd  20717  pntrlog2bnd  20735  pntpbnd1  20737  pntlemj  20754  pntlemf  20756  abvcxp  20766  padicabv  20781  padicabvcxp  20783  grpoidinvlem3  20875  grpolcan  20902  isgrp2d  20904  ghsubgolem  21039  nvmul0or  21212  nvelbl  21264  nvelbl2  21265  sspmval  21311  sspival  21316  sspimsval  21318  nmoub3i  21353  blocnilem  21384  sspph  21435  ubthlem1  21451  ubthlem3  21453  minvecolem3  21457  hvmul0or  21606  hvaddsub4  21659  shsel3  21896  shsel1  21902  spansncol  22149  chscllem2  22219  5oalem2  22236  5oalem4  22238  3oalem2  22244  hoaddcl  22340  eigposi  22418  nmopub2tALT  22491  unoplin  22502  nmfnleub2  22508  hmopadj2  22523  hmoplin  22524  kbpj  22538  eighmorth  22546  0cnop  22561  0cnfn  22562  lnconi  22615  nlelchi  22643  riesz3i  22644  cnlnadjlem6  22654  adjadd  22675  branmfn  22687  bra11  22690  leop2  22706  leopadd  22714  leopmuli  22715  leoptri  22718  leopnmid  22720  nmopleid  22721  opsqrlem1  22722  hmopidmchi  22733  pjss2coi  22746  pjssdif1i  22757  pj3si  22789  pj3cor1i  22791  hstle  22812  hstrlem3a  22842  cvcon3  22866  mdbr2  22878  dmdbr2  22885  mddmd2  22891  mdslmd2i  22912  csmdsymi  22916  superpos  22936  atordi  22966  atcvatlem  22967  chirredlem1  22972  chirredi  22976  mdsymlem1  22985  mdsymlem2  22986  mdsymlem3  22987  mdsymlem4  22988  mdsymlem5  22989  sumdmdii  22997  cdj3i  23023  ballotlemic  23067  ballotlem1c  23068  ballotlemsv  23070  ballotlemsima  23076  opfv  23192  xppreima  23213  xrmulc1cn  23305  rge0scvg  23375  lmxrge0  23377  lmdvg  23378  gsumpropd2lem  23381  hashge1  23390  esumpr2  23441  esumpcvgval  23448  esumcvg  23456  measdivcstOLD  23553  measdivcst  23554  subfacp1lem5  23717  divelunit  24082  dedekind  24084  fundmpss  24124  dfon2lem8  24148  poseq  24255  soseq  24256  wfrlem4  24261  frrlem4  24286  sltval2  24312  nocvxminlem  24346  nobndup  24356  nobnddown  24357  brcgr  24530  eqeelen  24534  brbtwn2  24535  colinearalglem4  24539  colinearalg  24540  axcgrid  24546  axsegconlem3  24549  axcontlem2  24595  axcontlem8  24601  hfext  24815  supaddc  24927  supadd  24928  lxflflp1  24932  itg2addnclem  24933  itg2addnclem2  24934  areacirclem4  24938  areacirclem6  24941  npincppr  25170  cbicp  25177  toplat  25301  trran2  25404  ltrran2  25414  ltrinvlem  25417  usptoplem  25557  istopx  25558  prcnt  25562  addidv2  25668  imonclem  25824  elicc3  26239  opnregcld  26259  filnetlem4  26341  eqfnun  26398  upixp  26414  indexdom  26424  fipreimaOLD  26426  filbcmb  26443  fzadd2  26455  sdclem1  26464  fdc  26466  fdc1  26467  incsequz  26469  nnubfi  26471  nninfnub  26472  csbrn  26473  metf1o  26480  geomcau  26486  sstotbnd2  26509  equivtotbnd  26513  isbnd3b  26520  bndss  26521  equivbnd  26525  equivbnd2  26527  prdsbnd  26528  prdstotbnd  26529  prdsbnd2  26530  cntotbnd  26531  ismtycnv  26537  heibor1  26545  heiborlem1  26546  bfplem2  26558  bfp  26559  rrnmet  26564  rrndstprj1  26565  rrncmslem  26567  rrnequiv  26570  ghomco  26584  grpokerinj  26586  isdrngo2  26600  rngohomco  26616  riscer  26630  idlsubcl  26659  keridl  26668  ispridl2  26674  igenval2  26702  isfldidl  26704  ispridlc  26706  pridlc3  26709  dmncan1  26712  isnacs3  26796  mzpexpmpt  26834  mzpindd  26835  mzpmfp  26836  rexzrexnn0  26896  fphpdo  26911  ctbnfien  26912  pellexlem5  26929  monotoddzzfi  27038  rmxnn  27049  setindtr  27128  pw2f1ocnv  27141  fnwe2  27161  kelac1  27172  dfac21  27175  islssfg2  27180  filnm  27203  dsmmsubg  27220  dsmmlss  27221  frlmup1  27261  isnumbasgrplem3  27281  lindff1  27301  islindf3  27307  rngunsnply  27389  f1otrspeq  27401  symggen  27422  psgnunilem2  27429  mndvass  27458  mndvlid  27459  mndvrid  27460  grpvlinv  27461  mamudi  27472  cncmpmax  27714  refsum2cnlem1  27719  fmuldfeq  27724  fmul01lt1lem1  27725  fmul01lt1lem2  27726  climinf  27743  climreeq  27750  stoweidlem14  27774  stoweidlem26  27786  stoweidlem27  27787  stoweidlem32  27792  stoweidlem42  27802  stoweidlem48  27808  stoweidlem61  27821  stoweidlem62  27822  stoweid  27823  stirlinglem5  27838  stirlinglem10  27843  uvtxnm1nbgra  28177  bnj605  29012  bnj1137  29098  lshpnelb  29247  lshpset2N  29382  isat3  29570  atnle  29580  islln2a  29779  2at0mat0  29787  pcl0bN  30185  cdlemg1cN  30849  diaglbN  31318  dib1dim2  31431  diclspsn  31457  dihlsscpre  31497  dihmeetALTN  31590  dihglblem6  31603  dochshpncl  31647  mapdval2N  31893  hdmap11lem2  32108
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