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  2145  ax11el  2146  ax11indalem  2149  ax11inda2ALT  2150  nfeud2  2168  pm2.61da2ne  2538  pm2.61da3ne  2539  uneqdifeq  3555  intab  3908  pofun  4346  tz7.7  4434  ordtr3  4453  ralxfrd  4564  onmindif2  4619  peano5  4695  poinxp  4769  relop  4850  soex  5138  fun11iun  5509  ssimaex  5600  fndmdif  5645  iinpreima  5671  fconst2g  5744  foeqcnvco  5820  f1eqcocnv  5821  isocnv  5843  grprinvd  6075  grpridd  6076  caofdi  6129  caofdir  6130  frxp  6241  riota2df  6341  riotasvdOLD  6364  riotasv2d  6365  tfrlem2  6408  oaordi  6560  oawordri  6564  oaass  6575  omlimcl  6592  odi  6593  omass  6594  oeordi  6601  oewordri  6606  oeoe  6613  nnaordi  6632  nnawordex  6651  nnaordex  6652  omsmolem  6667  omsmo  6668  xpdom2  6973  sbthlem9  6995  mapdom2  7048  ordunifi  7123  fiint  7149  fodomfib  7152  ordiso2  7246  unwdomg  7314  noinfepOLD  7377  cantnflem1c  7405  cantnflem1  7407  fidomtri  7642  dfac5  7771  dfac9  7778  ackbij2lem3  7883  cff1  7900  cfsmolem  7912  cfcoflem  7914  infpssrlem4  7948  fin23lem11  7959  fin23lem26  7967  fin23lem39  7992  axcc3  8080  axdc3lem2  8093  axdc3lem4  8095  zorn2lem6  8144  zorn2lem7  8145  fpwwe2lem10  8277  fpwwe2lem11  8278  fpwwe2lem12  8279  fpwwe2lem13  8280  fpwwe2  8281  intwun  8373  eltsk2g  8389  inatsk  8416  tskord  8418  r1tskina  8420  tskuni  8421  gruwun  8451  intgru  8452  grutsk1  8459  addcanpi  8539  mulcanpi  8540  indpi  8547  genpnmax  8647  addclprlem2  8657  mulclprlem  8659  supsrlem  8749  axpre-sup  8807  1re  8853  axsup  8914  00id  9003  addsubeq4  9082  divcan6  9483  ltmul12a  9628  lemul12b  9629  ledivdiv  9661  lediv12a  9665  lbinfm  9723  supmul1  9735  supmul  9738  nn2ge  9787  zrevaddcl  10079  zextle  10101  suprzcl  10107  fzind  10126  uz11  10266  uzwo3  10327  zbtwnre  10330  qreccl  10352  qrevaddcl  10354  irradd  10356  rpnnen1lem5  10362  xrlttr  10490  xaddass  10585  xleadd1a  10589  xlt2add  10596  xmulneg1  10605  xmulgt0  10619  xmulge0  10620  xmulasslem3  10622  xlemul1a  10624  xadddilem  10630  xrsupsslem  10641  xrinfmsslem  10642  xrub  10646  supxrun  10650  supxrunb1  10654  supxrbnd  10663  ixxin  10689  iccsplit  10784  iccshftr  10785  iccshftl  10787  iccdil  10789  icccntr  10791  fzaddel  10842  fzrev  10862  modadd1  11017  modmul1  11018  seqf2  11081  seqfeq2  11085  seqfeq  11087  sermono  11094  seqsplit  11095  seqcaopr2  11098  seqf1olem2a  11100  seqf1olem2  11102  seqid  11107  seqhomo  11109  seqz  11110  seqfeq3  11112  seqof  11119  expcllem  11130  mulexp  11157  expadd  11160  expaddz  11162  expmulz  11164  expdiv  11168  leexp1a  11176  expnlbnd  11247  bcpasc  11349  bccl  11350  hashdom  11377  hashfacen  11408  seqcoll  11417  revco  11505  cnpart  11741  sqrdiv  11767  lo1bdd2  12014  lo1bddrp  12015  lo1o1  12022  o1lo1  12027  o1lo12  12028  climrlim2  12037  rlimuni  12040  climshftlem  12064  rlimcld2  12068  rlimcn2  12080  climcn1  12081  rlimo1  12106  lo1add  12116  lo1mul  12117  climsqz  12130  climsqz2  12131  rlimsqzlem  12138  lo1le  12141  rlimno1  12143  clim2ser  12144  clim2ser2  12145  isermulc2  12147  climub  12151  isercolllem3  12156  serf0  12169  iseraltlem1  12170  iseralt  12173  sumeq2ii  12182  fsumcvg  12201  sumrb  12202  fsumf1o  12212  sumss  12213  fsumss  12214  fsumcvg3  12218  fsumcl2lem  12220  fsumcllem  12221  fsumadd  12227  fsumrev2  12260  fsum2mul  12267  fsum00  12272  fsumtscopo  12276  fsumparts  12280  fsumrlim  12285  fsumo1  12286  o1fsum  12287  iserabs  12289  isumsup2  12321  isumltss  12323  climcnds  12326  geomulcvg  12348  geoisum  12349  mertenslem1  12356  mertenslem2  12357  mertens  12358  eftlcvg  12402  rpnnen2lem5  12513  negdvdsb  12561  dvdsnegb  12562  fsumdvds  12588  dvdsext  12595  gcdcllem3  12708  dvdssq  12755  eucalgf  12769  phiprmpw  12860  eulerthlem2  12866  pc2dvds  12947  prmpwdvds  12967  prmreclem5  12983  prmreclem6  12984  1arith  12990  vdwlem6  13049  vdwnnlem3  13060  ramlb  13082  mreexmrid  13561  mreexexlem4d  13565  isacs2  13571  mreacs  13576  issubc  13728  funcres2b  13787  natpropd  13866  lubid  14132  poslubmo  14266  isacs4lem  14287  isacs5lem  14288  spwpr4  14356  mndpropd  14414  prdsidlem  14420  prdsmndd  14421  mhmpropd  14437  0mhm  14451  resmhm2  14453  resmhm2b  14454  pwsdiagmhm  14461  grplcan  14550  mulgnndir  14605  mulgnn0dir  14606  issubg2  14652  issubg4  14654  subgint  14657  ghmf1  14727  subgga  14770  gasubg  14772  cntzsubm  14827  odf1  14891  dfod2  14893  sylow1lem2  14926  sylow1lem3  14927  sylow3lem1  14954  frgpuplem  15097  frgpup1  15100  divsabl  15173  cyggenod  15187  cyggex2  15199  gsumval3  15207  gsumzaddlem  15219  prdsgsum  15245  dmdprd  15252  dprdfcntz  15266  dprdfeq0  15273  dprdlub  15277  dmdprdsplitlem  15288  dprd2da  15293  ablfac1c  15322  ablfac1eu  15324  rnglghm  15404  rngrghm  15405  gsumdixp  15408  irrednegb  15509  drngmul0or  15549  drngpropd  15555  issubrg2  15581  subrgint  15583  abvneg  15615  lmodvsghm  15702  lmodprop2d  15703  islss3  15732  lssintcl  15737  prdslmodd  15742  pwslmod  15743  pwsdiaglmhm  15830  lmhmpropd  15842  lvecvs0or  15877  lbsextlem2  15928  divsrhm  16005  unitrrg  16050  mplsubglem  16195  mplmonmul  16224  mplcoe1  16225  mplcoe2  16227  coe1tmmul  16369  cygznlem3  16539  ocvlss  16588  elcls  16826  opnssneib  16868  neissex  16880  maxlp  16894  tgrest  16906  restcld  16919  perfopn  16931  leordtval  16959  iscnp3  16990  cnpnei  17009  cnrest  17029  restcnrm  17106  lpcls  17108  llycmpkgen2  17261  1stckgenlem  17264  ptbasfi  17292  tx1cn  17319  xkoccn  17329  txcnp  17330  ptcnplem  17331  ptcn  17337  ptrescn  17349  kqt0lem  17443  isr0  17444  regr1lem2  17447  ptunhmeo  17515  trfbas2  17554  trfil2  17598  ufileu  17630  elfm3  17661  rnelfmlem  17663  cnflf  17713  fclsopn  17725  ufilcmp  17743  cnfcf  17753  alexsublem  17754  alexsub  17755  alexsubALTlem3  17759  alexsubALTlem4  17760  ptcmplem3  17764  ptcmplem5  17766  tmdmulg  17791  tgpmulg  17792  ghmcnp  17813  tsmsxplem1  17851  prdsxmetlem  17948  elbl3  17967  blin  17986  blssex  17989  blpnfctr  17998  prdsbl  18053  mopni2  18055  blsscls2  18066  metss  18070  stdbdmet  18078  metrest  18086  metcn  18105  txmetcn  18110  ngplcan  18148  isngp4  18149  ngppropd  18169  tngnm  18183  nmoid  18267  bl2ioo  18314  blcvx  18320  xrsxmet  18331  iocopnst  18454  icccvx  18464  evth2  18474  lebnumlem1  18475  pcoass  18538  pi1xfr  18569  pi1coghm  18575  nmoleub2lem  18611  tchcph  18683  lmmbr  18700  lmnn  18705  iscau2  18719  causs  18740  equivcfil  18741  lmle  18743  bcthlem4  18765  bcth2  18768  minveclem4  18812  ivthle  18832  ivthle2  18833  ovollb2lem  18863  ovoliunlem2  18878  ovolshftlem1  18884  ovolscalem1  18888  ovolicc2lem4  18895  ovolicc2lem5  18896  ioombl1lem4  18934  uniioombllem3  18956  uniioombllem4  18957  uniioombllem6  18959  dyaddisjlem  18966  vitalilem4  18982  ismbf  19001  mbfposb  19024  mbfsup  19035  mbfinf  19036  mbflimsup  19037  i1fd  19052  itg1val2  19055  itg1ge0  19057  itg1addlem4  19070  itg1addlem5  19071  i1fmulclem  19073  itg1mulc  19075  i1fres  19076  itg1climres  19085  mbfi1fseqlem4  19089  mbfi1flimlem  19093  mbfmullem2  19095  itg2seq  19113  itg2lea  19115  itg2splitlem  19119  itg2split  19120  itg2monolem1  19121  itg2monolem3  19123  itg2mono  19124  itg2i1fseqle  19125  itg2gt0  19131  itg2cnlem1  19132  itg2cn  19134  iblitg  19139  itgss  19182  itgeqa  19184  itgfsum  19197  iblabsr  19200  iblmulc2  19201  itgsplit  19206  itgsplitioo  19208  itgcn  19213  ditgsplitlem  19226  ditgsplit  19227  limciun  19260  dvcj  19315  dvfre  19316  dvlip  19356  lhop1lem  19376  lhop  19379  dvfsumle  19384  dvfsumge  19385  dvfsumabs  19386  dvfsumlem3  19391  dvfsumrlim  19394  dvfsumrlim2  19395  dvfsumrlim3  19396  ftc1lem1  19398  ftc1a  19400  ftc1lem4  19402  itgsubstlem  19411  evlslem1  19415  mpfind  19444  deg1leb  19497  elplyd  19600  plyeq0lem  19608  plypf1  19610  plyaddlem1  19611  plymullem1  19612  coeeulem  19622  plyco  19639  coeeq2  19640  dgrcolem1  19670  plydivlem2  19690  plydivlem4  19692  plydivex  19693  elqaalem2  19716  taylfvallem1  19752  dvtaylp  19765  mtest  19797  itgulm  19800  psergf  19804  pserulm  19814  psercn2  19815  pserdvlem2  19820  abelthlem8  19831  abelthlem9  19832  abssinper  19902  tanord  19916  advlogexp  20018  logtayllem  20022  logtayl  20023  cxpmul2z  20054  abscxp2  20056  angpined  20143  rlimcnp  20276  xrlimcnp  20279  efrlim  20280  rlimcxp  20284  emcllem7  20311  fsumharmonic  20321  wilthlem2  20323  ftalem1  20326  mumul  20435  fsumdvdsmul  20451  ppiub  20459  fsumvma  20468  dchrelbasd  20494  dchrsum2  20523  lgsval2lem  20561  lgsdir2  20583  lgsne0  20588  lgsquadlem1  20609  rpvmasumlem  20652  dchrisumlem2  20655  dchrisumlem3  20656  dchrisum  20657  dchrvmasumiflem1  20666  rpvmasum2  20677  dchrisum0re  20678  mudivsum  20695  mulogsum  20697  mulog2sumlem2  20700  pntrsumbnd  20731  pntrlog2bnd  20749  pntpbnd1  20751  pntlemj  20768  pntlemf  20770  abvcxp  20780  padicabv  20795  padicabvcxp  20797  grpoidinvlem3  20889  grpolcan  20916  isgrp2d  20918  ghsubgolem  21053  nvmul0or  21226  nvelbl  21278  nvelbl2  21279  sspmval  21325  sspival  21330  sspimsval  21332  nmoub3i  21367  blocnilem  21398  sspph  21449  ubthlem1  21465  ubthlem3  21467  minvecolem3  21471  hvmul0or  21620  hvaddsub4  21673  shsel3  21910  shsel1  21916  spansncol  22163  chscllem2  22233  5oalem2  22250  5oalem4  22252  3oalem2  22258  hoaddcl  22354  eigposi  22432  nmopub2tALT  22505  unoplin  22516  nmfnleub2  22522  hmopadj2  22537  hmoplin  22538  kbpj  22552  eighmorth  22560  0cnop  22575  0cnfn  22576  lnconi  22629  nlelchi  22657  riesz3i  22658  cnlnadjlem6  22668  adjadd  22689  branmfn  22701  bra11  22704  leop2  22720  leopadd  22728  leopmuli  22729  leoptri  22732  leopnmid  22734  nmopleid  22735  opsqrlem1  22736  hmopidmchi  22747  pjss2coi  22760  pjssdif1i  22771  pj3si  22803  pj3cor1i  22805  hstle  22826  hstrlem3a  22856  cvcon3  22880  mdbr2  22892  dmdbr2  22899  mddmd2  22905  mdslmd2i  22926  csmdsymi  22930  superpos  22950  atordi  22980  atcvatlem  22981  chirredlem1  22986  chirredi  22990  mdsymlem1  22999  mdsymlem2  23000  mdsymlem3  23001  mdsymlem4  23002  mdsymlem5  23003  sumdmdii  23011  cdj3i  23037  ballotlemic  23081  ballotlem1c  23082  ballotlemsv  23084  ballotlemsima  23090  opfv  23206  xppreima  23226  xrmulc1cn  23318  rge0scvg  23388  lmxrge0  23390  lmdvg  23391  gsumpropd2lem  23394  hashge1  23403  esumpr2  23454  esumpcvgval  23461  esumcvg  23469  measdivcstOLD  23566  measdivcst  23567  subfacp1lem5  23730  divelunit  24095  dedekind  24097  faclimlem7  24123  faclim  24126  cprodeq2ii  24135  prodrblem  24152  fprodcvg  24153  prodrblem2  24154  fprodf1o  24172  fundmpss  24193  dfon2lem8  24217  poseq  24324  soseq  24325  wfrlem4  24330  frrlem4  24355  sltval2  24381  nocvxminlem  24415  nobndup  24425  nobnddown  24426  brcgr  24600  eqeelen  24604  brbtwn2  24605  colinearalglem4  24609  colinearalg  24610  axcgrid  24616  axsegconlem3  24619  axcontlem2  24665  axcontlem8  24671  hfext  24885  supaddc  24995  supadd  24996  lxflflp1  25000  itg2addnclem  25003  itg2addnclem2  25004  iblabsnclem  25014  iblmulc2nc  25016  ftc1cnnclem  25024  areacirclem4  25030  areacirclem6  25033  npincppr  25262  cbicp  25269  toplat  25393  trran2  25496  ltrran2  25506  ltrinvlem  25509  usptoplem  25649  istopx  25650  prcnt  25654  addidv2  25760  imonclem  25916  elicc3  26331  opnregcld  26351  filnetlem4  26433  eqfnun  26490  upixp  26506  indexdom  26516  fipreimaOLD  26518  filbcmb  26535  fzadd2  26547  sdclem1  26556  fdc  26558  fdc1  26559  incsequz  26561  nnubfi  26563  nninfnub  26564  csbrn  26565  metf1o  26572  geomcau  26578  sstotbnd2  26601  equivtotbnd  26605  isbnd3b  26612  bndss  26613  equivbnd  26617  equivbnd2  26619  prdsbnd  26620  prdstotbnd  26621  prdsbnd2  26622  cntotbnd  26623  ismtycnv  26629  heibor1  26637  heiborlem1  26638  bfplem2  26650  bfp  26651  rrnmet  26656  rrndstprj1  26657  rrncmslem  26659  rrnequiv  26662  ghomco  26676  grpokerinj  26678  isdrngo2  26692  rngohomco  26708  riscer  26722  idlsubcl  26751  keridl  26760  ispridl2  26766  igenval2  26794  isfldidl  26796  ispridlc  26798  pridlc3  26801  dmncan1  26804  isnacs3  26888  mzpexpmpt  26926  mzpindd  26927  mzpmfp  26928  rexzrexnn0  26988  fphpdo  27003  ctbnfien  27004  pellexlem5  27021  monotoddzzfi  27130  rmxnn  27141  setindtr  27220  pw2f1ocnv  27233  fnwe2  27253  kelac1  27264  dfac21  27267  islssfg2  27272  filnm  27295  dsmmsubg  27312  dsmmlss  27313  frlmup1  27353  isnumbasgrplem3  27373  lindff1  27393  islindf3  27399  rngunsnply  27481  f1otrspeq  27493  symggen  27514  psgnunilem2  27521  mndvass  27550  mndvlid  27551  mndvrid  27552  grpvlinv  27553  mamudi  27564  cncmpmax  27806  refsum2cnlem1  27811  fmuldfeq  27816  fmul01lt1lem1  27817  fmul01lt1lem2  27818  climinf  27835  climreeq  27842  stoweidlem14  27866  stoweidlem26  27878  stoweidlem27  27879  stoweidlem32  27884  stoweidlem42  27894  stoweidlem48  27900  stoweidlem61  27913  stoweidlem62  27914  stoweid  27915  stirlinglem5  27930  stirlinglem10  27935  uvtxnm1nbgra  28307  bnj605  29255  bnj1137  29341  lshpnelb  29796  lshpset2N  29931  isat3  30119  atnle  30129  islln2a  30328  2at0mat0  30336  pcl0bN  30734  cdlemg1cN  31398  diaglbN  31867  dib1dim2  31980  diclspsn  32006  dihlsscpre  32046  dihmeetALTN  32139  dihglblem6  32152  dochshpncl  32196  mapdval2N  32442  hdmap11lem2  32657
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