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  2243  ax11el  2244  ax11indalem  2247  ax11inda2ALT  2248  nfeud2  2266  pm2.61da2ne  2646  pm2.61da3ne  2647  uneqdifeq  3676  intab  4040  pofun  4479  tz7.7  4567  ordtr3  4586  ralxfrd  4696  onmindif2  4751  peano5  4827  poinxp  4900  relop  4982  soex  5278  fun11iun  5654  ssimaex  5747  fndmdif  5793  iinpreima  5819  fconst2g  5905  foeqcnvco  5986  f1eqcocnv  5987  isocnv  6009  grprinvd  6245  grpridd  6246  caofdi  6299  caofdir  6300  f1o2ndf1  6413  frxp  6415  riota2df  6529  riotasvdOLD  6552  riotasv2d  6553  tfrlem2  6596  oaordi  6748  oawordri  6752  oaass  6763  omlimcl  6780  odi  6781  omass  6782  oeordi  6789  oewordri  6794  oeoe  6801  nnaordi  6820  nnawordex  6839  nnaordex  6840  omsmolem  6855  omsmo  6856  xpdom2  7162  sbthlem9  7184  mapdom2  7237  ordunifi  7316  fiint  7342  fodomfib  7345  ordiso2  7440  unwdomg  7508  noinfepOLD  7571  cantnflem1c  7599  cantnflem1  7601  fidomtri  7836  dfac5  7965  dfac9  7972  ackbij2lem3  8077  cff1  8094  cfsmolem  8106  cfcoflem  8108  infpssrlem4  8142  fin23lem11  8153  fin23lem26  8161  fin23lem39  8186  axcc3  8274  axdc3lem2  8287  axdc3lem4  8289  zorn2lem6  8337  zorn2lem7  8338  fpwwe2lem10  8470  fpwwe2lem11  8471  fpwwe2lem12  8472  fpwwe2lem13  8473  fpwwe2  8474  intwun  8566  eltsk2g  8582  inatsk  8609  tskord  8611  r1tskina  8613  tskuni  8614  gruwun  8644  intgru  8645  grutsk1  8652  addcanpi  8732  mulcanpi  8733  indpi  8740  genpnmax  8840  addclprlem2  8850  mulclprlem  8852  supsrlem  8942  axpre-sup  9000  1re  9046  axsup  9107  00id  9197  addsubeq4  9276  divcan6  9677  ltmul12a  9822  lemul12b  9823  ledivdiv  9855  lediv12a  9859  lbinfm  9917  supmul1  9929  supmul  9932  nn2ge  9981  zrevaddcl  10277  zextle  10299  suprzcl  10305  fzind  10324  uz11  10464  uzwo3  10525  zbtwnre  10528  qreccl  10550  qrevaddcl  10552  irradd  10554  rpnnen1lem5  10560  xrlttr  10689  xaddass  10784  xleadd1a  10788  xlt2add  10795  xmulneg1  10804  xmulgt0  10818  xmulge0  10819  xmulasslem3  10821  xlemul1a  10823  xadddilem  10829  xrsupsslem  10841  xrinfmsslem  10842  xrub  10846  supxrun  10850  supxrunb1  10854  supxrbnd  10863  ixxin  10889  iccsplit  10985  iccshftr  10986  iccshftl  10988  iccdil  10990  icccntr  10992  fzaddel  11043  fzrev  11064  modadd1  11233  modmul1  11234  seqf2  11297  seqfeq2  11301  seqfeq  11303  sermono  11310  seqsplit  11311  seqcaopr2  11314  seqf1olem2a  11316  seqf1olem2  11318  seqid  11323  seqhomo  11325  seqz  11326  seqfeq3  11328  seqof  11335  expcllem  11347  mulexp  11374  expadd  11377  expaddz  11379  expmulz  11381  expdiv  11385  leexp1a  11393  expnlbnd  11464  bcpasc  11567  bccl  11568  hashdom  11608  hashge1  11618  hashfacen  11658  seqcoll  11667  revco  11758  cnpart  12000  sqrdiv  12026  lo1bdd2  12273  lo1bddrp  12274  lo1o1  12281  o1lo1  12286  o1lo12  12287  climrlim2  12296  rlimuni  12299  climshftlem  12323  rlimcld2  12327  rlimcn2  12339  climcn1  12340  rlimo1  12365  lo1add  12375  lo1mul  12376  climsqz  12389  climsqz2  12390  rlimsqzlem  12397  lo1le  12400  rlimno1  12402  clim2ser  12403  clim2ser2  12404  isermulc2  12406  climub  12410  isercolllem3  12415  serf0  12429  iseraltlem1  12430  iseralt  12433  sumeq2ii  12442  fsumcvg  12461  sumrb  12462  fsumf1o  12472  sumss  12473  fsumss  12474  fsumcvg3  12478  fsumcl2lem  12480  fsumcllem  12481  fsumadd  12487  fsumrev2  12520  fsum2mul  12527  fsum00  12532  fsumtscopo  12536  fsumparts  12540  fsumrlim  12545  fsumo1  12546  o1fsum  12547  iserabs  12549  isumsup2  12581  isumltss  12583  climcnds  12586  geomulcvg  12608  geoisum  12609  mertenslem1  12616  mertenslem2  12617  mertens  12618  eftlcvg  12662  rpnnen2lem5  12773  negdvdsb  12821  dvdsnegb  12822  fsumdvds  12848  dvdsext  12855  gcdcllem3  12968  dvdssq  13015  eucalgf  13029  phiprmpw  13120  eulerthlem2  13126  pc2dvds  13207  prmpwdvds  13227  prmreclem5  13243  prmreclem6  13244  1arith  13250  vdwlem6  13309  vdwnnlem3  13320  ramlb  13342  mreexmrid  13823  mreexexlem4d  13827  isacs2  13833  mreacs  13838  issubc  13990  funcres2b  14049  natpropd  14128  lubid  14394  poslubmo  14528  isacs4lem  14549  isacs5lem  14550  spwpr4  14618  mndpropd  14676  prdsidlem  14682  prdsmndd  14683  mhmpropd  14699  0mhm  14713  resmhm2  14715  resmhm2b  14716  pwsdiagmhm  14723  grplcan  14812  mulgnndir  14867  mulgnn0dir  14868  issubg2  14914  issubg4  14916  subgint  14919  ghmf1  14989  subgga  15032  gasubg  15034  cntzsubm  15089  odf1  15153  dfod2  15155  sylow1lem2  15188  sylow1lem3  15189  sylow3lem1  15216  frgpuplem  15359  frgpup1  15362  divsabl  15435  cyggenod  15449  cyggex2  15461  gsumval3  15469  gsumzaddlem  15481  prdsgsum  15507  dmdprd  15514  dprdfcntz  15528  dprdfeq0  15535  dprdlub  15539  dmdprdsplitlem  15550  dprd2da  15555  ablfac1c  15584  ablfac1eu  15586  rnglghm  15666  rngrghm  15667  gsumdixp  15670  irrednegb  15771  drngmul0or  15811  drngpropd  15817  issubrg2  15843  subrgint  15845  abvneg  15877  lmodvsghm  15960  lmodprop2d  15961  islss3  15990  lssintcl  15995  prdslmodd  16000  pwslmod  16001  pwsdiaglmhm  16088  lmhmpropd  16100  lvecvs0or  16135  lbsextlem2  16186  divsrhm  16263  unitrrg  16308  mplsubglem  16453  mplmonmul  16482  mplcoe1  16483  mplcoe2  16485  coe1tmmul  16624  cygznlem3  16805  ocvlss  16854  elcls  17092  opnssneib  17134  neissex  17146  maxlp  17165  tgrest  17177  restcld  17190  perfopn  17203  leordtval  17231  iscnp3  17262  cnpnei  17282  cnrest  17303  restcnrm  17380  lpcls  17382  llycmpkgen2  17535  1stckgenlem  17538  ptbasfi  17566  tx1cn  17594  xkoccn  17604  txcnp  17605  ptcnplem  17606  ptcn  17612  ptrescn  17624  kqt0lem  17721  isr0  17722  regr1lem2  17725  ptunhmeo  17793  trfbas2  17828  trfil2  17872  ufileu  17904  elfm3  17935  rnelfmlem  17937  cnflf  17987  fclsopn  17999  ufilcmp  18017  cnfcf  18027  alexsublem  18028  alexsub  18029  alexsubALTlem3  18033  alexsubALTlem4  18034  ptcmplem3  18038  ptcmplem5  18040  cnextcn  18051  tmdmulg  18075  tgpmulg  18076  ghmcnp  18097  tsmsxplem1  18135  trust  18212  ustuqtop4  18227  ucnima  18264  ucncn  18268  prdsxmetlem  18351  elbl3ps  18374  elbl3  18375  blin  18404  blssexps  18409  blssex  18410  blpnfctr  18419  prdsbl  18474  mopni2  18476  blsscls2  18487  metss  18491  stdbdmet  18499  metrest  18507  metcn  18526  txmetcn  18531  ngplcan  18610  isngp4  18611  ngppropd  18631  tngnm  18645  nmoid  18729  bl2ioo  18776  blcvx  18782  xrsxmet  18793  iocopnst  18918  icccvx  18928  evth2  18938  lebnumlem1  18939  pcoass  19002  pi1xfr  19033  pi1coghm  19039  nmoleub2lem  19075  tchcph  19147  lmmbr  19164  lmnn  19169  iscau2  19183  causs  19204  equivcfil  19205  lmle  19207  bcthlem4  19233  cmetcuspOLD  19260  minveclem4  19286  ivthle  19306  ivthle2  19307  ovollb2lem  19337  ovoliunlem2  19352  ovolshftlem1  19358  ovolscalem1  19362  ovolicc2lem4  19369  ovolicc2lem5  19370  ioombl1lem4  19408  uniioombllem3  19430  uniioombllem4  19431  uniioombllem6  19433  dyaddisjlem  19440  vitalilem4  19456  ismbf  19475  mbfposb  19498  mbfsup  19509  mbfinf  19510  mbflimsup  19511  i1fd  19526  itg1val2  19529  itg1ge0  19531  itg1addlem4  19544  itg1addlem5  19545  i1fmulclem  19547  itg1mulc  19549  i1fres  19550  itg1climres  19559  mbfi1fseqlem4  19563  mbfi1flimlem  19567  mbfmullem2  19569  itg2seq  19587  itg2lea  19589  itg2splitlem  19593  itg2split  19594  itg2monolem1  19595  itg2monolem3  19597  itg2mono  19598  itg2i1fseqle  19599  itg2gt0  19605  itg2cnlem1  19606  itg2cn  19608  iblitg  19613  itgss  19656  itgeqa  19658  itgfsum  19671  iblabsr  19674  iblmulc2  19675  itgsplit  19680  itgsplitioo  19682  itgcn  19687  ditgsplitlem  19700  ditgsplit  19701  limciun  19734  dvcj  19789  dvfre  19790  dvlip  19830  lhop1lem  19850  lhop  19853  dvfsumle  19858  dvfsumge  19859  dvfsumabs  19860  dvfsumlem3  19865  dvfsumrlim  19868  dvfsumrlim2  19869  dvfsumrlim3  19870  ftc1lem1  19872  ftc1a  19874  ftc1lem4  19876  itgsubstlem  19885  evlslem1  19889  mpfind  19918  deg1leb  19971  elplyd  20074  plyeq0lem  20082  plypf1  20084  plyaddlem1  20085  plymullem1  20086  coeeulem  20096  plyco  20113  coeeq2  20114  dgrcolem1  20144  plydivlem2  20164  plydivlem4  20166  plydivex  20167  elqaalem2  20190  taylfvallem1  20226  dvtaylp  20239  mtest  20273  itgulm  20277  psergf  20281  pserulm  20291  psercn2  20292  pserdvlem2  20297  abelthlem8  20308  abelthlem9  20309  abssinper  20379  tanord  20393  advlogexp  20499  logtayllem  20503  logtayl  20504  cxpmul2z  20535  abscxp2  20537  angpined  20624  rlimcnp  20757  xrlimcnp  20760  efrlim  20761  rlimcxp  20765  emcllem7  20793  fsumharmonic  20803  wilthlem2  20805  ftalem1  20808  mumul  20917  fsumdvdsmul  20933  ppiub  20941  fsumvma  20950  dchrelbasd  20976  dchrsum2  21005  lgsval2lem  21043  lgsdir2  21065  lgsne0  21070  lgsquadlem1  21091  rpvmasumlem  21134  dchrisumlem2  21137  dchrisumlem3  21138  dchrisum  21139  dchrvmasumiflem1  21148  rpvmasum2  21159  dchrisum0re  21160  mudivsum  21177  mulogsum  21179  mulog2sumlem2  21182  pntrsumbnd  21213  pntrlog2bnd  21231  pntpbnd1  21233  pntlemj  21250  pntlemf  21252  abvcxp  21262  padicabv  21277  padicabvcxp  21279  usgraidx2vlem2  21364  nbgraf1olem5  21408  usgramaxsize  21449  uvtxnm1nbgra  21456  2trllemH  21505  2trllemE  21506  grpoidinvlem3  21747  grpolcan  21774  isgrp2d  21776  ghsubgolem  21911  nvmul0or  22086  nvelbl  22138  nvelbl2  22139  sspmval  22185  sspival  22190  sspimsval  22192  nmoub3i  22227  blocnilem  22258  sspph  22309  ubthlem1  22325  ubthlem3  22327  minvecolem3  22331  hvmul0or  22480  hvaddsub4  22533  shsel3  22770  shsel1  22776  spansncol  23023  chscllem2  23093  5oalem2  23110  5oalem4  23112  3oalem2  23118  hoaddcl  23214  eigposi  23292  nmopub2tALT  23365  unoplin  23376  nmfnleub2  23382  hmopadj2  23397  hmoplin  23398  kbpj  23412  eighmorth  23420  0cnop  23435  0cnfn  23436  lnconi  23489  nlelchi  23517  riesz3i  23518  cnlnadjlem6  23528  adjadd  23549  branmfn  23561  bra11  23564  leop2  23580  leopadd  23588  leopmuli  23589  leoptri  23592  leopnmid  23594  nmopleid  23595  opsqrlem1  23596  hmopidmchi  23607  pjss2coi  23620  pjssdif1i  23631  pj3si  23663  pj3cor1i  23665  hstle  23686  hstrlem3a  23716  cvcon3  23740  mdbr2  23752  dmdbr2  23759  mddmd2  23765  mdslmd2i  23786  csmdsymi  23790  superpos  23810  atordi  23840  atcvatlem  23841  chirredlem1  23846  chirredi  23850  mdsymlem1  23859  mdsymlem2  23860  mdsymlem3  23861  mdsymlem4  23862  mdsymlem5  23863  sumdmdii  23871  cdj3i  23897  opfv  24011  xppreima  24012  toslub  24144  tosglb  24145  gsumpropd2lem  24173  pstmfval  24244  pstmxmet  24245  cnvordtrestixx  24264  xrmulc1cn  24269  rge0scvg  24288  lmxrge0  24290  lmdvg  24291  qqhcn  24328  gsumesum  24404  esumpr2  24411  esumfsup  24413  esumpcvgval  24421  hasheuni  24428  esumcvg  24429  measdivcstOLD  24531  measdivcst  24532  voliune  24538  volfiniune  24539  volmeas  24540  ballotlemic  24717  ballotlem1c  24718  ballotlemsv  24720  ballotlemsima  24726  lgamgulmlem6  24771  lgamgulm2  24773  subfacp1lem5  24823  divelunit  25138  dedekind  25140  clim2div  25170  ntrivcvg  25178  ntrivcvgtail  25181  prodeq2ii  25192  prodrblem  25208  fprodcvg  25209  prodrblem2  25210  prodmo  25215  fprodf1o  25225  prodss  25226  fprodss  25227  fprodcl2lem  25229  fprodcllem  25230  fprodabs  25250  fprodefsum  25251  fprodeq0  25252  fprod2d  25258  iprodclim3  25266  iprodmul  25269  risefacp1  25297  fallfacp1  25298  faclim  25313  faclim2  25315  fundmpss  25336  dfon2lem8  25360  poseq  25467  soseq  25468  wfrlem4  25473  frrlem4  25498  sltval2  25524  nocvxminlem  25558  nobndup  25568  nobnddown  25569  brcgr  25743  eqeelen  25747  brbtwn2  25748  colinearalglem4  25752  colinearalg  25753  axcgrid  25759  axsegconlem3  25762  axcontlem8  25814  hfext  26028  supaddc  26137  supadd  26138  lxflflp1  26142  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  mbfresfi  26152  itg2addnclem  26155  itg2addnclem2  26156  itg2addnc  26158  iblabsnclem  26167  iblmulc2nc  26169  ftc1cnnclem  26177  areacirclem4  26183  areacirclem6  26186  elicc3  26210  opnregcld  26223  filnetlem4  26300  eqfnun  26313  upixp  26321  indexdom  26326  filbcmb  26332  fzadd2  26335  sdclem1  26337  fdc  26339  fdc1  26340  incsequz  26342  nnubfi  26344  nninfnub  26345  csbrn  26346  metf1o  26351  geomcau  26355  sstotbnd2  26373  equivtotbnd  26377  isbnd3b  26384  bndss  26385  equivbnd  26389  equivbnd2  26391  prdsbnd  26392  prdstotbnd  26393  prdsbnd2  26394  cntotbnd  26395  ismtycnv  26401  heibor1  26409  heiborlem1  26410  bfplem2  26422  bfp  26423  rrnmet  26428  rrndstprj1  26429  rrncmslem  26431  rrnequiv  26434  ghomco  26448  grpokerinj  26450  isdrngo2  26464  rngohomco  26480  riscer  26494  idlsubcl  26523  keridl  26532  ispridl2  26538  igenval2  26566  isfldidl  26568  ispridlc  26570  pridlc3  26573  dmncan1  26576  isnacs3  26654  mzpexpmpt  26692  mzpindd  26693  mzpmfp  26694  rexzrexnn0  26754  fphpdo  26768  ctbnfien  26769  pellexlem5  26786  monotoddzzfi  26895  rmxnn  26906  setindtr  26985  pw2f1ocnv  26998  fnwe2  27018  kelac1  27029  dfac21  27032  islssfg2  27037  filnm  27060  dsmmsubg  27077  dsmmlss  27078  frlmup1  27118  isnumbasgrplem3  27138  lindff1  27158  islindf3  27164  rngunsnply  27246  f1otrspeq  27258  symggen  27279  psgnunilem2  27286  mndvass  27315  mndvlid  27316  mndvrid  27317  grpvlinv  27318  mamudi  27329  cncmpmax  27570  refsum2cnlem1  27575  fmuldfeq  27580  fmul01lt1lem1  27581  fmul01lt1lem2  27582  climinf  27599  climreeq  27606  stoweidlem14  27630  stoweidlem20  27636  stoweidlem26  27642  stoweidlem27  27643  stoweidlem31  27647  stoweidlem32  27648  stoweidlem34  27650  stoweidlem35  27651  stoweidlem42  27658  stoweidlem43  27659  stoweidlem46  27662  stoweidlem48  27664  stoweidlem52  27668  stoweidlem53  27669  stoweidlem54  27670  stoweidlem55  27671  stoweidlem56  27672  stoweidlem57  27673  stoweidlem58  27674  stoweidlem59  27675  stoweidlem60  27676  stoweidlem61  27677  stoweidlem62  27678  stoweid  27679  wallispilem3  27683  stirlinglem5  27694  stirlinglem10  27699  elfzmlbp  27978  swrd0swrd  28009  swrdccat3b  28031  usgra2adedgspthlem2  28044  usgra2adedgspth  28045  el2wlksotot  28079  vdgn1frgrav2  28131  2spotdisj  28164  frghash2spot  28166  usgreghash2spotv  28169  bnj605  28984  bnj1137  29070  lshpnelb  29467  lshpset2N  29602  isat3  29790  atnle  29800  islln2a  29999  2at0mat0  30007  pcl0bN  30405  cdlemg1cN  31069  diaglbN  31538  dib1dim2  31651  diclspsn  31677  dihlsscpre  31717  dihmeetALTN  31810  dihglblem6  31823  dochshpncl  31867  mapdval2N  32113  hdmap11lem2  32328
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