MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adantlr Structured version   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  2269  ax11el  2270  ax11indalem  2273  ax11inda2ALT  2274  nfeud2  2292  pm2.61da2ne  2677  pm2.61da3ne  2678  uneqdifeq  3708  intab  4072  pofun  4511  tz7.7  4599  ordtr3  4618  ralxfrd  4729  onmindif2  4784  peano5  4860  poinxp  4933  relop  5015  soex  5311  fun11iun  5687  ssimaex  5780  fndmdif  5826  iinpreima  5852  fconst2g  5938  foeqcnvco  6019  f1eqcocnv  6020  isocnv  6042  grprinvd  6278  grpridd  6279  caofdi  6332  caofdir  6333  f1o2ndf1  6446  frxp  6448  riota2df  6562  riotasvdOLD  6585  riotasv2d  6586  tfrlem2  6629  oaordi  6781  oawordri  6785  oaass  6796  omlimcl  6813  odi  6814  omass  6815  oeordi  6822  oewordri  6827  oeoe  6834  nnaordi  6853  nnawordex  6872  nnaordex  6873  omsmolem  6888  omsmo  6889  xpdom2  7195  sbthlem9  7217  mapdom2  7270  ordunifi  7349  fiint  7375  fodomfib  7378  ordiso2  7476  unwdomg  7544  noinfepOLD  7607  cantnflem1c  7635  cantnflem1  7637  fidomtri  7872  dfac5  8001  dfac9  8008  ackbij2lem3  8113  cff1  8130  cfsmolem  8142  cfcoflem  8144  infpssrlem4  8178  fin23lem11  8189  fin23lem26  8197  fin23lem39  8222  axcc3  8310  axdc3lem2  8323  axdc3lem4  8325  zorn2lem6  8373  zorn2lem7  8374  fpwwe2lem10  8506  fpwwe2lem11  8507  fpwwe2lem12  8508  fpwwe2lem13  8509  fpwwe2  8510  intwun  8602  eltsk2g  8618  inatsk  8645  tskord  8647  r1tskina  8649  tskuni  8650  gruwun  8680  intgru  8681  grutsk1  8688  addcanpi  8768  mulcanpi  8769  indpi  8776  genpnmax  8876  addclprlem2  8886  mulclprlem  8888  supsrlem  8978  axpre-sup  9036  1re  9082  axsup  9143  00id  9233  addsubeq4  9312  divcan6  9713  ltmul12a  9858  lemul12b  9859  ledivdiv  9891  lediv12a  9895  lbinfm  9953  supmul1  9965  supmul  9968  nn2ge  10017  zrevaddcl  10313  zextle  10335  suprzcl  10341  fzind  10360  uz11  10500  uzwo3  10561  zbtwnre  10564  qreccl  10586  qrevaddcl  10588  irradd  10590  rpnnen1lem5  10596  xrlttr  10725  xaddass  10820  xleadd1a  10824  xlt2add  10831  xmulneg1  10840  xmulgt0  10854  xmulge0  10855  xmulasslem3  10857  xlemul1a  10859  xadddilem  10865  xrsupsslem  10877  xrinfmsslem  10878  xrub  10882  supxrun  10886  supxrunb1  10890  supxrbnd  10899  ixxin  10925  iccsplit  11021  iccshftr  11022  iccshftl  11024  iccdil  11026  icccntr  11028  fzaddel  11079  fzrev  11100  modadd1  11270  modmul1  11271  seqf2  11334  seqfeq2  11338  seqfeq  11340  sermono  11347  seqsplit  11348  seqcaopr2  11351  seqf1olem2a  11353  seqf1olem2  11355  seqid  11360  seqhomo  11362  seqz  11363  seqfeq3  11365  seqof  11372  expcllem  11384  mulexp  11411  expadd  11414  expaddz  11416  expmulz  11418  expdiv  11422  leexp1a  11430  expnlbnd  11501  bcpasc  11604  bccl  11605  hashdom  11645  hashge1  11655  hashfacen  11695  seqcoll  11704  revco  11795  cnpart  12037  sqrdiv  12063  lo1bdd2  12310  lo1bddrp  12311  lo1o1  12318  o1lo1  12323  o1lo12  12324  climrlim2  12333  rlimuni  12336  climshftlem  12360  rlimcld2  12364  rlimcn2  12376  climcn1  12377  rlimo1  12402  lo1add  12412  lo1mul  12413  climsqz  12426  climsqz2  12427  rlimsqzlem  12434  lo1le  12437  rlimno1  12439  clim2ser  12440  clim2ser2  12441  isermulc2  12443  climub  12447  isercolllem3  12452  serf0  12466  iseraltlem1  12467  iseralt  12470  sumeq2ii  12479  fsumcvg  12498  sumrb  12499  fsumf1o  12509  sumss  12510  fsumss  12511  fsumcvg3  12515  fsumcl2lem  12517  fsumcllem  12518  fsumadd  12524  fsumrev2  12557  fsum2mul  12564  fsum00  12569  fsumtscopo  12573  fsumparts  12577  fsumrlim  12582  fsumo1  12583  o1fsum  12584  iserabs  12586  isumsup2  12618  isumltss  12620  climcnds  12623  geomulcvg  12645  geoisum  12646  mertenslem1  12653  mertenslem2  12654  mertens  12655  eftlcvg  12699  rpnnen2lem5  12810  negdvdsb  12858  dvdsnegb  12859  fsumdvds  12885  dvdsext  12892  gcdcllem3  13005  dvdssq  13052  eucalgf  13066  phiprmpw  13157  eulerthlem2  13163  pc2dvds  13244  prmpwdvds  13264  prmreclem5  13280  prmreclem6  13281  1arith  13287  vdwlem6  13346  vdwnnlem3  13357  ramlb  13379  mreexmrid  13860  mreexexlem4d  13864  isacs2  13870  mreacs  13875  issubc  14027  funcres2b  14086  natpropd  14165  lubid  14431  poslubmo  14565  isacs4lem  14586  isacs5lem  14587  spwpr4  14655  mndpropd  14713  prdsidlem  14719  prdsmndd  14720  mhmpropd  14736  0mhm  14750  resmhm2  14752  resmhm2b  14753  pwsdiagmhm  14760  grplcan  14849  mulgnndir  14904  mulgnn0dir  14905  issubg2  14951  issubg4  14953  subgint  14956  ghmf1  15026  subgga  15069  gasubg  15071  cntzsubm  15126  odf1  15190  dfod2  15192  sylow1lem2  15225  sylow1lem3  15226  sylow3lem1  15253  frgpuplem  15396  frgpup1  15399  divsabl  15472  cyggenod  15486  cyggex2  15498  gsumval3  15506  gsumzaddlem  15518  prdsgsum  15544  dmdprd  15551  dprdfcntz  15565  dprdfeq0  15572  dprdlub  15576  dmdprdsplitlem  15587  dprd2da  15592  ablfac1c  15621  ablfac1eu  15623  rnglghm  15703  rngrghm  15704  gsumdixp  15707  irrednegb  15808  drngmul0or  15848  drngpropd  15854  issubrg2  15880  subrgint  15882  abvneg  15914  lmodvsghm  15997  lmodprop2d  15998  islss3  16027  lssintcl  16032  prdslmodd  16037  pwslmod  16038  pwsdiaglmhm  16125  lmhmpropd  16137  lvecvs0or  16172  lbsextlem2  16223  divsrhm  16300  unitrrg  16345  mplsubglem  16490  mplmonmul  16519  mplcoe1  16520  mplcoe2  16522  coe1tmmul  16661  cygznlem3  16842  ocvlss  16891  elcls  17129  opnssneib  17171  neissex  17183  maxlp  17203  tgrest  17215  restcld  17228  perfopn  17241  leordtval  17269  iscnp3  17300  cnpnei  17320  cnrest  17341  restcnrm  17418  lpcls  17420  llycmpkgen2  17574  1stckgenlem  17577  ptbasfi  17605  tx1cn  17633  xkoccn  17643  txcnp  17644  ptcnplem  17645  ptcn  17651  ptrescn  17663  kqt0lem  17760  isr0  17761  regr1lem2  17764  ptunhmeo  17832  trfbas2  17867  trfil2  17911  ufileu  17943  elfm3  17974  rnelfmlem  17976  cnflf  18026  fclsopn  18038  ufilcmp  18056  cnfcf  18066  alexsublem  18067  alexsub  18068  alexsubALTlem3  18072  alexsubALTlem4  18073  ptcmplem3  18077  ptcmplem5  18079  cnextcn  18090  tmdmulg  18114  tgpmulg  18115  ghmcnp  18136  tsmsxplem1  18174  trust  18251  ustuqtop4  18266  ucnima  18303  ucncn  18307  prdsxmetlem  18390  elbl3ps  18413  elbl3  18414  blin  18443  blssexps  18448  blssex  18449  blpnfctr  18458  prdsbl  18513  mopni2  18515  blsscls2  18526  metss  18530  stdbdmet  18538  metrest  18546  metcn  18565  txmetcn  18570  ngplcan  18649  isngp4  18650  ngppropd  18670  tngnm  18684  nmoid  18768  bl2ioo  18815  blcvx  18821  xrsxmet  18832  iocopnst  18957  icccvx  18967  evth2  18977  lebnumlem1  18978  pcoass  19041  pi1xfr  19072  pi1coghm  19078  nmoleub2lem  19114  tchcph  19186  lmmbr  19203  lmnn  19208  iscau2  19222  causs  19243  equivcfil  19244  lmle  19246  bcthlem4  19272  cmetcuspOLD  19299  minveclem4  19325  ivthle  19345  ivthle2  19346  ovollb2lem  19376  ovoliunlem2  19391  ovolshftlem1  19397  ovolscalem1  19401  ovolicc2lem4  19408  ovolicc2lem5  19409  ioombl1lem4  19447  uniioombllem3  19469  uniioombllem4  19470  uniioombllem6  19472  dyaddisjlem  19479  vitalilem4  19495  ismbf  19514  mbfposb  19537  mbfsup  19548  mbfinf  19549  mbflimsup  19550  i1fd  19565  itg1val2  19568  itg1ge0  19570  itg1addlem4  19583  itg1addlem5  19584  i1fmulclem  19586  itg1mulc  19588  i1fres  19589  itg1climres  19598  mbfi1fseqlem4  19602  mbfi1flimlem  19606  mbfmullem2  19608  itg2seq  19626  itg2lea  19628  itg2splitlem  19632  itg2split  19633  itg2monolem1  19634  itg2monolem3  19636  itg2mono  19637  itg2i1fseqle  19638  itg2gt0  19644  itg2cnlem1  19645  itg2cn  19647  iblitg  19652  itgss  19695  itgeqa  19697  itgfsum  19710  iblabsr  19713  iblmulc2  19714  itgsplit  19719  itgsplitioo  19721  itgcn  19726  ditgsplitlem  19739  ditgsplit  19740  limciun  19773  dvcj  19828  dvfre  19829  dvlip  19869  lhop1lem  19889  lhop  19892  dvfsumle  19897  dvfsumge  19898  dvfsumabs  19899  dvfsumlem3  19904  dvfsumrlim  19907  dvfsumrlim2  19908  dvfsumrlim3  19909  ftc1lem1  19911  ftc1a  19913  ftc1lem4  19915  itgsubstlem  19924  evlslem1  19928  mpfind  19957  deg1leb  20010  elplyd  20113  plyeq0lem  20121  plypf1  20123  plyaddlem1  20124  plymullem1  20125  coeeulem  20135  plyco  20152  coeeq2  20153  dgrcolem1  20183  plydivlem2  20203  plydivlem4  20205  plydivex  20206  elqaalem2  20229  taylfvallem1  20265  dvtaylp  20278  mtest  20312  itgulm  20316  psergf  20320  pserulm  20330  psercn2  20331  pserdvlem2  20336  abelthlem8  20347  abelthlem9  20348  abssinper  20418  tanord  20432  advlogexp  20538  logtayllem  20542  logtayl  20543  cxpmul2z  20574  abscxp2  20576  angpined  20663  rlimcnp  20796  xrlimcnp  20799  efrlim  20800  rlimcxp  20804  emcllem7  20832  fsumharmonic  20842  wilthlem2  20844  ftalem1  20847  mumul  20956  fsumdvdsmul  20972  ppiub  20980  fsumvma  20989  dchrelbasd  21015  dchrsum2  21044  lgsval2lem  21082  lgsdir2  21104  lgsne0  21109  lgsquadlem1  21130  rpvmasumlem  21173  dchrisumlem2  21176  dchrisumlem3  21177  dchrisum  21178  dchrvmasumiflem1  21187  rpvmasum2  21198  dchrisum0re  21199  mudivsum  21216  mulogsum  21218  mulog2sumlem2  21221  pntrsumbnd  21252  pntrlog2bnd  21270  pntpbnd1  21272  pntlemj  21289  pntlemf  21291  abvcxp  21301  padicabv  21316  padicabvcxp  21318  usgraidx2vlem2  21403  nbgraf1olem5  21447  usgramaxsize  21488  uvtxnm1nbgra  21495  2trllemH  21544  2trllemE  21545  grpoidinvlem3  21786  grpolcan  21813  isgrp2d  21815  ghsubgolem  21950  nvmul0or  22125  nvelbl  22177  nvelbl2  22178  sspmval  22224  sspival  22229  sspimsval  22231  nmoub3i  22266  blocnilem  22297  sspph  22348  ubthlem1  22364  ubthlem3  22366  minvecolem3  22370  hvmul0or  22519  hvaddsub4  22572  shsel3  22809  shsel1  22815  spansncol  23062  chscllem2  23132  5oalem2  23149  5oalem4  23151  3oalem2  23157  hoaddcl  23253  eigposi  23331  nmopub2tALT  23404  unoplin  23415  nmfnleub2  23421  hmopadj2  23436  hmoplin  23437  kbpj  23451  eighmorth  23459  0cnop  23474  0cnfn  23475  lnconi  23528  nlelchi  23556  riesz3i  23557  cnlnadjlem6  23567  adjadd  23588  branmfn  23600  bra11  23603  leop2  23619  leopadd  23627  leopmuli  23628  leoptri  23631  leopnmid  23633  nmopleid  23634  opsqrlem1  23635  hmopidmchi  23646  pjss2coi  23659  pjssdif1i  23670  pj3si  23702  pj3cor1i  23704  hstle  23725  hstrlem3a  23755  cvcon3  23779  mdbr2  23791  dmdbr2  23798  mddmd2  23804  mdslmd2i  23825  csmdsymi  23829  superpos  23849  atordi  23879  atcvatlem  23880  chirredlem1  23885  chirredi  23889  mdsymlem1  23898  mdsymlem2  23899  mdsymlem3  23900  mdsymlem4  23901  mdsymlem5  23902  sumdmdii  23910  cdj3i  23936  opfv  24050  xppreima  24051  toslub  24183  tosglb  24184  gsumpropd2lem  24212  pstmfval  24283  pstmxmet  24284  cnvordtrestixx  24303  xrmulc1cn  24308  rge0scvg  24327  lmxrge0  24329  lmdvg  24330  qqhcn  24367  gsumesum  24443  esumpr2  24450  esumfsup  24452  esumpcvgval  24460  hasheuni  24467  esumcvg  24468  measdivcstOLD  24570  measdivcst  24571  voliune  24577  volfiniune  24578  volmeas  24579  ballotlemic  24756  ballotlem1c  24757  ballotlemsv  24759  ballotlemsima  24765  lgamgulmlem6  24810  lgamgulm2  24812  subfacp1lem5  24862  divelunit  25177  dedekind  25179  clim2div  25209  ntrivcvg  25217  ntrivcvgtail  25220  prodeq2ii  25231  prodrblem  25247  fprodcvg  25248  prodrblem2  25249  prodmo  25254  fprodf1o  25264  prodss  25265  fprodss  25266  fprodcl2lem  25268  fprodcllem  25269  fprodabs  25289  fprodefsum  25290  fprodeq0  25291  fprod2d  25297  iprodclim3  25305  iprodmul  25308  risefacp1  25337  fallfacp1  25338  faclim  25357  faclim2  25359  fundmpss  25382  dfon2lem8  25409  poseq  25520  soseq  25521  wfrlem4  25533  frrlem4  25577  sltval2  25603  nocvxminlem  25637  nobndup  25647  nobnddown  25648  brcgr  25831  eqeelen  25835  brbtwn2  25836  colinearalglem4  25840  colinearalg  25841  axcgrid  25847  axsegconlem3  25850  axcontlem8  25902  hfext  26116  supaddc  26228  supadd  26229  lxflflp1  26233  mblfinlem  26234  mblfinlem2  26235  mblfinlem3  26236  ismblfin  26237  mbfresfi  26243  itg2addnclem  26246  itg2addnclem2  26247  itg2addnc  26249  iblabsnclem  26258  iblmulc2nc  26260  ftc1cnnclem  26268  ftc1anclem1  26270  ftc1anclem2  26271  ftc1anclem3  26272  ftc1anclem4  26273  ftc1anclem5  26274  ftc1anclem6  26275  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278  ftc2nc  26279  areacirclem4  26284  areacirclem6  26287  elicc3  26311  opnregcld  26324  filnetlem4  26401  eqfnun  26414  upixp  26422  indexdom  26427  filbcmb  26433  fzadd2  26436  sdclem1  26438  fdc  26440  fdc1  26441  incsequz  26443  nnubfi  26445  nninfnub  26446  csbrn  26447  metf1o  26452  geomcau  26456  sstotbnd2  26474  equivtotbnd  26478  isbnd3b  26485  bndss  26486  equivbnd  26490  equivbnd2  26492  prdsbnd  26493  prdstotbnd  26494  prdsbnd2  26495  cntotbnd  26496  ismtycnv  26502  heibor1  26510  heiborlem1  26511  bfplem2  26523  bfp  26524  rrnmet  26529  rrndstprj1  26530  rrncmslem  26532  rrnequiv  26535  ghomco  26549  grpokerinj  26551  isdrngo2  26565  rngohomco  26581  riscer  26595  idlsubcl  26624  keridl  26633  ispridl2  26639  igenval2  26667  isfldidl  26669  ispridlc  26671  pridlc3  26674  dmncan1  26677  isnacs3  26755  mzpexpmpt  26793  mzpindd  26794  mzpmfp  26795  rexzrexnn0  26855  fphpdo  26869  ctbnfien  26870  pellexlem5  26887  monotoddzzfi  26996  rmxnn  27007  setindtr  27086  pw2f1ocnv  27099  fnwe2  27119  kelac1  27129  dfac21  27132  islssfg2  27137  filnm  27160  dsmmsubg  27177  dsmmlss  27178  frlmup1  27218  isnumbasgrplem3  27238  lindff1  27258  islindf3  27264  rngunsnply  27346  f1otrspeq  27358  symggen  27379  psgnunilem2  27386  mndvass  27415  mndvlid  27416  mndvrid  27417  grpvlinv  27418  mamudi  27429  cncmpmax  27670  refsum2cnlem1  27675  fmuldfeq  27680  fmul01lt1lem1  27681  fmul01lt1lem2  27682  climinf  27699  climreeq  27706  stoweidlem14  27730  stoweidlem20  27736  stoweidlem26  27742  stoweidlem27  27743  stoweidlem31  27747  stoweidlem32  27748  stoweidlem34  27750  stoweidlem35  27751  stoweidlem42  27758  stoweidlem43  27759  stoweidlem46  27762  stoweidlem48  27764  stoweidlem52  27768  stoweidlem53  27769  stoweidlem54  27770  stoweidlem55  27771  stoweidlem56  27772  stoweidlem57  27773  stoweidlem58  27774  stoweidlem59  27775  stoweidlem60  27776  stoweidlem61  27777  stoweidlem62  27778  stoweid  27779  wallispilem3  27783  stirlinglem5  27794  stirlinglem10  27799  elfzmlbp  28091  2elfz2melfz  28101  swrd0swrd  28163  swrdccat  28182  usgra2adedgspthlem2  28267  usgra2adedgspth  28268  el2wlksotot  28302  vdgn1frgrav2  28354  2spotdisj  28387  frghash2spot  28389  usgreghash2spotv  28392  bnj605  29215  bnj1137  29301  lshpnelb  29719  lshpset2N  29854  isat3  30042  atnle  30052  islln2a  30251  2at0mat0  30259  pcl0bN  30657  cdlemg1cN  31321  diaglbN  31790  dib1dim2  31903  diclspsn  31929  dihlsscpre  31969  dihmeetALTN  32062  dihglblem6  32075  dochshpncl  32119  mapdval2N  32365  hdmap11lem2  32580
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