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

Theorem adantlr 696
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 444 . 2  |-  ( (
ph  /\  th )  ->  ph )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan 458 1  |-  ( ( ( ph  /\  th )  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  ad2antrr  707  ad2ant2r  728  ad2ant2rl  730  pm2.61ddan  768  pm2.61dda  769  3ad2antl1  1119  3ad2antl2  1120  3adant1r  1177  ax11eq  2220  ax11el  2221  ax11indalem  2224  ax11inda2ALT  2225  nfeud2  2243  pm2.61da2ne  2622  pm2.61da3ne  2623  uneqdifeq  3652  intab  4015  pofun  4453  tz7.7  4541  ordtr3  4560  ralxfrd  4670  onmindif2  4725  peano5  4801  poinxp  4874  relop  4956  soex  5252  fun11iun  5628  ssimaex  5720  fndmdif  5766  iinpreima  5792  fconst2g  5878  foeqcnvco  5959  f1eqcocnv  5960  isocnv  5982  grprinvd  6218  grpridd  6219  caofdi  6272  caofdir  6273  frxp  6385  riota2df  6499  riotasvdOLD  6522  riotasv2d  6523  tfrlem2  6566  oaordi  6718  oawordri  6722  oaass  6733  omlimcl  6750  odi  6751  omass  6752  oeordi  6759  oewordri  6764  oeoe  6771  nnaordi  6790  nnawordex  6809  nnaordex  6810  omsmolem  6825  omsmo  6826  xpdom2  7132  sbthlem9  7154  mapdom2  7207  ordunifi  7286  fiint  7312  fodomfib  7315  ordiso2  7410  unwdomg  7478  noinfepOLD  7541  cantnflem1c  7569  cantnflem1  7571  fidomtri  7806  dfac5  7935  dfac9  7942  ackbij2lem3  8047  cff1  8064  cfsmolem  8076  cfcoflem  8078  infpssrlem4  8112  fin23lem11  8123  fin23lem26  8131  fin23lem39  8156  axcc3  8244  axdc3lem2  8257  axdc3lem4  8259  zorn2lem6  8307  zorn2lem7  8308  fpwwe2lem10  8440  fpwwe2lem11  8441  fpwwe2lem12  8442  fpwwe2lem13  8443  fpwwe2  8444  intwun  8536  eltsk2g  8552  inatsk  8579  tskord  8581  r1tskina  8583  tskuni  8584  gruwun  8614  intgru  8615  grutsk1  8622  addcanpi  8702  mulcanpi  8703  indpi  8710  genpnmax  8810  addclprlem2  8820  mulclprlem  8822  supsrlem  8912  axpre-sup  8970  1re  9016  axsup  9077  00id  9166  addsubeq4  9245  divcan6  9646  ltmul12a  9791  lemul12b  9792  ledivdiv  9824  lediv12a  9828  lbinfm  9886  supmul1  9898  supmul  9901  nn2ge  9950  zrevaddcl  10246  zextle  10268  suprzcl  10274  fzind  10293  uz11  10433  uzwo3  10494  zbtwnre  10497  qreccl  10519  qrevaddcl  10521  irradd  10523  rpnnen1lem5  10529  xrlttr  10658  xaddass  10753  xleadd1a  10757  xlt2add  10764  xmulneg1  10773  xmulgt0  10787  xmulge0  10788  xmulasslem3  10790  xlemul1a  10792  xadddilem  10798  xrsupsslem  10810  xrinfmsslem  10811  xrub  10815  supxrun  10819  supxrunb1  10823  supxrbnd  10832  ixxin  10858  iccsplit  10954  iccshftr  10955  iccshftl  10957  iccdil  10959  icccntr  10961  fzaddel  11012  fzrev  11032  modadd1  11198  modmul1  11199  seqf2  11262  seqfeq2  11266  seqfeq  11268  sermono  11275  seqsplit  11276  seqcaopr2  11279  seqf1olem2a  11281  seqf1olem2  11283  seqid  11288  seqhomo  11290  seqz  11291  seqfeq3  11293  seqof  11300  expcllem  11312  mulexp  11339  expadd  11342  expaddz  11344  expmulz  11346  expdiv  11350  leexp1a  11358  expnlbnd  11429  bcpasc  11532  bccl  11533  hashdom  11573  hashge1  11583  hashfacen  11623  seqcoll  11632  revco  11723  cnpart  11965  sqrdiv  11991  lo1bdd2  12238  lo1bddrp  12239  lo1o1  12246  o1lo1  12251  o1lo12  12252  climrlim2  12261  rlimuni  12264  climshftlem  12288  rlimcld2  12292  rlimcn2  12304  climcn1  12305  rlimo1  12330  lo1add  12340  lo1mul  12341  climsqz  12354  climsqz2  12355  rlimsqzlem  12362  lo1le  12365  rlimno1  12367  clim2ser  12368  clim2ser2  12369  isermulc2  12371  climub  12375  isercolllem3  12380  serf0  12394  iseraltlem1  12395  iseralt  12398  sumeq2ii  12407  fsumcvg  12426  sumrb  12427  fsumf1o  12437  sumss  12438  fsumss  12439  fsumcvg3  12443  fsumcl2lem  12445  fsumcllem  12446  fsumadd  12452  fsumrev2  12485  fsum2mul  12492  fsum00  12497  fsumtscopo  12501  fsumparts  12505  fsumrlim  12510  fsumo1  12511  o1fsum  12512  iserabs  12514  isumsup2  12546  isumltss  12548  climcnds  12551  geomulcvg  12573  geoisum  12574  mertenslem1  12581  mertenslem2  12582  mertens  12583  eftlcvg  12627  rpnnen2lem5  12738  negdvdsb  12786  dvdsnegb  12787  fsumdvds  12813  dvdsext  12820  gcdcllem3  12933  dvdssq  12980  eucalgf  12994  phiprmpw  13085  eulerthlem2  13091  pc2dvds  13172  prmpwdvds  13192  prmreclem5  13208  prmreclem6  13209  1arith  13215  vdwlem6  13274  vdwnnlem3  13285  ramlb  13307  mreexmrid  13788  mreexexlem4d  13792  isacs2  13798  mreacs  13803  issubc  13955  funcres2b  14014  natpropd  14093  lubid  14359  poslubmo  14493  isacs4lem  14514  isacs5lem  14515  spwpr4  14583  mndpropd  14641  prdsidlem  14647  prdsmndd  14648  mhmpropd  14664  0mhm  14678  resmhm2  14680  resmhm2b  14681  pwsdiagmhm  14688  grplcan  14777  mulgnndir  14832  mulgnn0dir  14833  issubg2  14879  issubg4  14881  subgint  14884  ghmf1  14954  subgga  14997  gasubg  14999  cntzsubm  15054  odf1  15118  dfod2  15120  sylow1lem2  15153  sylow1lem3  15154  sylow3lem1  15181  frgpuplem  15324  frgpup1  15327  divsabl  15400  cyggenod  15414  cyggex2  15426  gsumval3  15434  gsumzaddlem  15446  prdsgsum  15472  dmdprd  15479  dprdfcntz  15493  dprdfeq0  15500  dprdlub  15504  dmdprdsplitlem  15515  dprd2da  15520  ablfac1c  15549  ablfac1eu  15551  rnglghm  15631  rngrghm  15632  gsumdixp  15635  irrednegb  15736  drngmul0or  15776  drngpropd  15782  issubrg2  15808  subrgint  15810  abvneg  15842  lmodvsghm  15925  lmodprop2d  15926  islss3  15955  lssintcl  15960  prdslmodd  15965  pwslmod  15966  pwsdiaglmhm  16053  lmhmpropd  16065  lvecvs0or  16100  lbsextlem2  16151  divsrhm  16228  unitrrg  16273  mplsubglem  16418  mplmonmul  16447  mplcoe1  16448  mplcoe2  16450  coe1tmmul  16589  cygznlem3  16766  ocvlss  16815  elcls  17053  opnssneib  17095  neissex  17107  maxlp  17126  tgrest  17138  restcld  17151  perfopn  17164  leordtval  17192  iscnp3  17223  cnpnei  17243  cnrest  17264  restcnrm  17341  lpcls  17343  llycmpkgen2  17496  1stckgenlem  17499  ptbasfi  17527  tx1cn  17555  xkoccn  17565  txcnp  17566  ptcnplem  17567  ptcn  17573  ptrescn  17585  kqt0lem  17682  isr0  17683  regr1lem2  17686  ptunhmeo  17754  trfbas2  17789  trfil2  17833  ufileu  17865  elfm3  17896  rnelfmlem  17898  cnflf  17948  fclsopn  17960  ufilcmp  17978  cnfcf  17988  alexsublem  17989  alexsub  17990  alexsubALTlem3  17994  alexsubALTlem4  17995  ptcmplem3  17999  ptcmplem5  18001  cnextcn  18012  tmdmulg  18036  tgpmulg  18037  ghmcnp  18058  tsmsxplem1  18096  trust  18173  ustuqtop4  18188  ucnima  18225  ucncn  18229  prdsxmetlem  18299  elbl3  18318  blin  18337  blssex  18340  blpnfctr  18349  prdsbl  18404  mopni2  18406  blsscls2  18417  metss  18421  stdbdmet  18429  metrest  18437  metcn  18456  txmetcn  18461  ngplcan  18521  isngp4  18522  ngppropd  18542  tngnm  18556  nmoid  18640  bl2ioo  18687  blcvx  18693  xrsxmet  18704  iocopnst  18829  icccvx  18839  evth2  18849  lebnumlem1  18850  pcoass  18913  pi1xfr  18944  pi1coghm  18950  nmoleub2lem  18986  tchcph  19058  lmmbr  19075  lmnn  19080  iscau2  19094  causs  19115  equivcfil  19116  lmle  19118  bcthlem4  19142  cmetcusp  19168  minveclem4  19193  ivthle  19213  ivthle2  19214  ovollb2lem  19244  ovoliunlem2  19259  ovolshftlem1  19265  ovolscalem1  19269  ovolicc2lem4  19276  ovolicc2lem5  19277  ioombl1lem4  19315  uniioombllem3  19337  uniioombllem4  19338  uniioombllem6  19340  dyaddisjlem  19347  vitalilem4  19363  ismbf  19382  mbfposb  19405  mbfsup  19416  mbfinf  19417  mbflimsup  19418  i1fd  19433  itg1val2  19436  itg1ge0  19438  itg1addlem4  19451  itg1addlem5  19452  i1fmulclem  19454  itg1mulc  19456  i1fres  19457  itg1climres  19466  mbfi1fseqlem4  19470  mbfi1flimlem  19474  mbfmullem2  19476  itg2seq  19494  itg2lea  19496  itg2splitlem  19500  itg2split  19501  itg2monolem1  19502  itg2monolem3  19504  itg2mono  19505  itg2i1fseqle  19506  itg2gt0  19512  itg2cnlem1  19513  itg2cn  19515  iblitg  19520  itgss  19563  itgeqa  19565  itgfsum  19578  iblabsr  19581  iblmulc2  19582  itgsplit  19587  itgsplitioo  19589  itgcn  19594  ditgsplitlem  19607  ditgsplit  19608  limciun  19641  dvcj  19696  dvfre  19697  dvlip  19737  lhop1lem  19757  lhop  19760  dvfsumle  19765  dvfsumge  19766  dvfsumabs  19767  dvfsumlem3  19772  dvfsumrlim  19775  dvfsumrlim2  19776  dvfsumrlim3  19777  ftc1lem1  19779  ftc1a  19781  ftc1lem4  19783  itgsubstlem  19792  evlslem1  19796  mpfind  19825  deg1leb  19878  elplyd  19981  plyeq0lem  19989  plypf1  19991  plyaddlem1  19992  plymullem1  19993  coeeulem  20003  plyco  20020  coeeq2  20021  dgrcolem1  20051  plydivlem2  20071  plydivlem4  20073  plydivex  20074  elqaalem2  20097  taylfvallem1  20133  dvtaylp  20146  mtest  20180  itgulm  20184  psergf  20188  pserulm  20198  psercn2  20199  pserdvlem2  20204  abelthlem8  20215  abelthlem9  20216  abssinper  20286  tanord  20300  advlogexp  20406  logtayllem  20410  logtayl  20411  cxpmul2z  20442  abscxp2  20444  angpined  20531  rlimcnp  20664  xrlimcnp  20667  efrlim  20668  rlimcxp  20672  emcllem7  20700  fsumharmonic  20710  wilthlem2  20712  ftalem1  20715  mumul  20824  fsumdvdsmul  20840  ppiub  20848  fsumvma  20857  dchrelbasd  20883  dchrsum2  20912  lgsval2lem  20950  lgsdir2  20972  lgsne0  20977  lgsquadlem1  20998  rpvmasumlem  21041  dchrisumlem2  21044  dchrisumlem3  21045  dchrisum  21046  dchrvmasumiflem1  21055  rpvmasum2  21066  dchrisum0re  21067  mudivsum  21084  mulogsum  21086  mulog2sumlem2  21089  pntrsumbnd  21120  pntrlog2bnd  21138  pntpbnd1  21140  pntlemj  21157  pntlemf  21159  abvcxp  21169  padicabv  21184  padicabvcxp  21186  usgraidx2vlem2  21270  nbgraf1olem5  21314  usgramaxsize  21355  uvtxnm1nbgra  21362  grpoidinvlem3  21635  grpolcan  21662  isgrp2d  21664  ghsubgolem  21799  nvmul0or  21974  nvelbl  22026  nvelbl2  22027  sspmval  22073  sspival  22078  sspimsval  22080  nmoub3i  22115  blocnilem  22146  sspph  22197  ubthlem1  22213  ubthlem3  22215  minvecolem3  22219  hvmul0or  22368  hvaddsub4  22421  shsel3  22658  shsel1  22664  spansncol  22911  chscllem2  22981  5oalem2  22998  5oalem4  23000  3oalem2  23006  hoaddcl  23102  eigposi  23180  nmopub2tALT  23253  unoplin  23264  nmfnleub2  23270  hmopadj2  23285  hmoplin  23286  kbpj  23300  eighmorth  23308  0cnop  23323  0cnfn  23324  lnconi  23377  nlelchi  23405  riesz3i  23406  cnlnadjlem6  23416  adjadd  23437  branmfn  23449  bra11  23452  leop2  23468  leopadd  23476  leopmuli  23477  leoptri  23480  leopnmid  23482  nmopleid  23483  opsqrlem1  23484  hmopidmchi  23495  pjss2coi  23508  pjssdif1i  23519  pj3si  23551  pj3cor1i  23553  hstle  23574  hstrlem3a  23604  cvcon3  23628  mdbr2  23640  dmdbr2  23647  mddmd2  23653  mdslmd2i  23674  csmdsymi  23678  superpos  23698  atordi  23728  atcvatlem  23729  chirredlem1  23734  chirredi  23738  mdsymlem1  23747  mdsymlem2  23748  mdsymlem3  23749  mdsymlem4  23750  mdsymlem5  23751  sumdmdii  23759  cdj3i  23785  opfv  23893  xppreima  23894  gsumpropd2lem  24042  cnvordtrestixx  24108  xrmulc1cn  24113  rge0scvg  24132  lmxrge0  24134  lmdvg  24135  qqhcn  24167  gsumesum  24240  esumpr2  24247  esumfsup  24249  esumpcvgval  24257  hasheuni  24264  esumcvg  24265  measdivcstOLD  24365  measdivcst  24366  voliune  24372  volfiniune  24373  volmeas  24374  ballotlemic  24536  ballotlem1c  24537  ballotlemsv  24539  ballotlemsima  24545  lgamgulmlem6  24590  lgamgulm2  24592  subfacp1lem5  24642  divelunit  24957  dedekind  24959  clim2div  24989  ntrivcvg  24997  ntrivcvgtail  25000  prodeq2ii  25011  prodrblem  25027  fprodcvg  25028  prodrblem2  25029  prodmo  25034  fprodf1o  25044  prodss  25045  fprodss  25046  fprodcl2lem  25048  fprodcllem  25049  fprodabs  25069  fprodefsum  25070  fprodeq0  25071  iprodclim3  25078  iprodmul  25081  risefacp1  25106  fallfacp1  25107  faclim  25116  faclim2  25118  fundmpss  25139  dfon2lem8  25163  poseq  25270  soseq  25271  wfrlem4  25276  frrlem4  25301  sltval2  25327  nocvxminlem  25361  nobndup  25371  nobnddown  25372  brcgr  25546  eqeelen  25550  brbtwn2  25551  colinearalglem4  25555  colinearalg  25556  axcgrid  25562  axsegconlem3  25565  axcontlem8  25617  hfext  25831  supaddc  25940  supadd  25941  lxflflp1  25945  itg2addnclem  25950  itg2addnclem2  25951  iblabsnclem  25961  iblmulc2nc  25963  ftc1cnnclem  25971  areacirclem4  25977  areacirclem6  25980  elicc3  26004  opnregcld  26017  filnetlem4  26094  eqfnun  26107  upixp  26115  indexdom  26120  filbcmb  26126  fzadd2  26129  sdclem1  26131  fdc  26133  fdc1  26134  incsequz  26136  nnubfi  26138  nninfnub  26139  csbrn  26140  metf1o  26145  geomcau  26149  sstotbnd2  26167  equivtotbnd  26171  isbnd3b  26178  bndss  26179  equivbnd  26183  equivbnd2  26185  prdsbnd  26186  prdstotbnd  26187  prdsbnd2  26188  cntotbnd  26189  ismtycnv  26195  heibor1  26203  heiborlem1  26204  bfplem2  26216  bfp  26217  rrnmet  26222  rrndstprj1  26223  rrncmslem  26225  rrnequiv  26228  ghomco  26242  grpokerinj  26244  isdrngo2  26258  rngohomco  26274  riscer  26288  idlsubcl  26317  keridl  26326  ispridl2  26332  igenval2  26360  isfldidl  26362  ispridlc  26364  pridlc3  26367  dmncan1  26370  isnacs3  26448  mzpexpmpt  26486  mzpindd  26487  mzpmfp  26488  rexzrexnn0  26548  fphpdo  26562  ctbnfien  26563  pellexlem5  26580  monotoddzzfi  26689  rmxnn  26700  setindtr  26779  pw2f1ocnv  26792  fnwe2  26812  kelac1  26823  dfac21  26826  islssfg2  26831  filnm  26854  dsmmsubg  26871  dsmmlss  26872  frlmup1  26912  isnumbasgrplem3  26932  lindff1  26952  islindf3  26958  rngunsnply  27040  f1otrspeq  27052  symggen  27073  psgnunilem2  27080  mndvass  27109  mndvlid  27110  mndvrid  27111  grpvlinv  27112  mamudi  27123  cncmpmax  27364  refsum2cnlem1  27369  fmuldfeq  27374  fmul01lt1lem1  27375  fmul01lt1lem2  27376  climinf  27393  climreeq  27400  stoweidlem14  27424  stoweidlem20  27430  stoweidlem26  27436  stoweidlem27  27437  stoweidlem31  27441  stoweidlem32  27442  stoweidlem34  27444  stoweidlem35  27445  stoweidlem42  27452  stoweidlem43  27453  stoweidlem46  27456  stoweidlem48  27458  stoweidlem52  27462  stoweidlem53  27463  stoweidlem54  27464  stoweidlem55  27465  stoweidlem56  27466  stoweidlem57  27467  stoweidlem58  27468  stoweidlem59  27469  stoweidlem60  27470  stoweidlem61  27471  stoweidlem62  27472  stoweid  27473  wallispilem3  27477  stirlinglem5  27488  stirlinglem10  27493  vdgn1frgrav2  27773  bnj605  28609  bnj1137  28695  lshpnelb  29150  lshpset2N  29285  isat3  29473  atnle  29483  islln2a  29682  2at0mat0  29690  pcl0bN  30088  cdlemg1cN  30752  diaglbN  31221  dib1dim2  31334  diclspsn  31360  dihlsscpre  31400  dihmeetALTN  31493  dihglblem6  31506  dochshpncl  31550  mapdval2N  31796  hdmap11lem2  32011
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