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

Theorem adantrr 698
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
adantrr  |-  ( (
ph  /\  ( ps  /\ 
th ) )  ->  ch )

Proof of Theorem adantrr
StepHypRef Expression
1 simpl 444 . 2  |-  ( ( ps  /\  th )  ->  ps )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan2 461 1  |-  ( (
ph  /\  ( ps  /\ 
th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  ad2ant2r  728  ad2ant2lr  729  consensus  926  3ad2antr1  1122  sbcom  2164  ax11eq  2269  ax11el  2270  po2nr  4508  sotric  4521  sotrieq  4522  tz7.7  4599  ordsucun  4797  fvtp1g  5934  fcof1o  6018  isocnv  6042  isores2  6045  isomin  6049  isoini  6050  f1oiso2  6064  ovmpt2df  6197  offval  6304  xp1st  6368  1stconst  6427  cnvf1olem  6436  fnse  6455  mpt2xopoveq  6462  oalim  6768  omlim  6769  oaass  6796  omordi  6801  omwordri  6807  odi  6814  oen0  6821  oewordri  6827  nnawordi  6856  nnmordi  6866  omabs  6882  erinxp  6970  dom2lem  7139  mapen  7263  ssenen  7273  ssfi  7321  domfi  7322  domunfican  7371  ordtypelem6  7484  ordtypelem7  7485  card2inf  7515  inf3lem6  7580  cantnfle  7618  cantnflem1b  7634  cantnflem1  7637  mapfien  7645  wemapwe  7646  rankxplim3  7797  fseqenlem2  7898  dfac5lem4  7999  dfac2  8003  cfsuc  8129  cfflb  8131  cofsmo  8141  infpssrlem4  8178  fin4en1  8181  ssfin4  8182  fin23lem26  8197  fin23lem22  8199  fin23lem27  8200  isf34lem4  8249  isf34lem5  8250  fin1a2lem12  8283  axdc3lem2  8323  axdc4lem  8327  ttukeylem6  8386  iundom2g  8407  pwcfsdom  8450  gchen2  8493  gchor  8494  fpwwe2lem7  8503  fpwwe2lem9  8505  fpwwe2lem11  8507  fpwwe2lem12  8508  fpwwe2  8510  pwfseqlem4  8529  gchina  8566  ltexprlem6  8910  prlem936  8916  mul4  9227  2addsub  9311  muladd  9458  ltleadd  9503  leord1  9546  eqord1  9547  ltord2  9548  leord2  9549  eqord2  9550  divmul3  9675  divcan7  9715  divadddiv  9721  lemul2a  9857  lemul12b  9859  ltmuldiv2  9873  ltdivmul  9874  ledivmul  9875  ltdivmul2  9877  lt2mul2div  9878  ledivmul2  9879  lemuldiv2  9882  lt2msq  9886  ltdiv23  9893  lediv23  9894  supmullem1  9966  infmrcl  9979  cju  9988  zextlt  10336  suprzcl  10341  zmax  10563  xrlttr  10725  xrre3  10751  qbtwnre  10777  xrsupsslem  10877  xrinfmsslem  10878  supxrunb1  10890  supxrunb2  10891  ixxdisj  10923  iooshf  10981  icodisj  11014  iccf1o  11031  modid  11262  modadd1  11270  modmul1  11271  seqf1o  11356  expsub  11419  sqlecan  11479  bcval5  11601  hashmap  11690  hashfacen  11695  seqcoll  11704  resqreu  12050  lenegsq  12116  limsupbnd2  12269  icco1  12326  rlimresb  12351  rlimsqzlem  12434  rlimsqz  12435  rlimsqz2  12436  caucvgrlem  12458  fsum0diag2  12558  o1fsum  12584  ruclem8  12828  dvdsmulcr  12871  ndvdsadd  12920  bitsshft  12979  hashdvds  13156  eulerthlem2  13163  pcqmul  13219  pcmpt  13253  prmreclem3  13278  4sqlem11  13315  0ram  13380  ramub1  13388  invfun  13981  coaval  14215  catcisolem  14253  prfcl  14292  prf1st  14293  prf2nd  14294  1st2ndprf  14295  curfuncf  14327  isposd  14404  lubun  14542  isacs3lem  14584  pslem  14630  psss  14638  spwpr4  14655  pwsdiagmhm  14760  gsumccat  14779  grpinvid1  14845  grpinvid2  14846  grplcan  14849  grplactcnv  14879  0nsg  14977  eqger  14982  resghm  15014  conjghm  15028  subgga  15069  gaorber  15077  gastacl  15078  orbsta  15082  odid  15168  odmulg  15184  gexid  15207  odcau  15230  lsmssv  15269  lsmcom2  15281  pj1ghm  15327  frgpuptf  15394  frgpup1  15399  ghmplusg  15453  cyggex2  15498  gsumval3eu  15505  gsumval3  15506  ablfac1eu  15623  pgpfac1lem5  15629  isdrngd  15852  issrngd  15941  lmhmf1o  16114  lmhmima  16115  lmhmpreima  16116  lspextmo  16124  lspdisj  16189  islbs3  16219  lbsextlem4  16225  drngnidl  16292  lidldvgen  16318  issubassa2  16395  psrbagconf1o  16431  evlslem2  16560  ply1sclf1  16672  cnsubrg  16751  znunit  16836  cygznlem3  16842  eltg2  17015  ntrss  17111  opncldf1  17140  ssnei2  17172  neindisj  17173  restopnb  17231  restntr  17238  tgcmp  17456  hauscmplem  17461  2ndc1stc  17506  2ndcdisj  17511  2ndcomap  17513  restlly  17538  lly1stc  17551  txcls  17628  txdis1cn  17659  pthaus  17662  txlm  17672  qtoptop2  17723  qtopomap  17742  kqt0lem  17760  pt1hmeo  17830  ptuncnv  17831  xkocnv  17838  fbasfip  17892  fgabs  17903  fbasrn  17908  elfm2  17972  fmfnfmlem2  17979  fmfnfmlem4  17981  ptcmplem3  18077  ptcmplem4  18078  tsmsres  18165  tsmsxplem1  18174  utoptop  18256  elbl2ps  18411  elbl2  18412  blin  18443  xmeter  18455  xmetresbl  18459  stdbdxmet  18537  metrest  18546  metustexhalfOLD  18585  metustexhalf  18586  dscmet  18612  nrmmetd  18614  tngngp2  18685  nmoi2  18756  icccmplem2  18846  reconnlem2  18850  metdstri  18873  metdsle  18874  metdsre  18875  metnrmlem3  18883  fsumcn  18892  icccvx  18967  bndth  18975  evth  18976  reparphti  19014  pi1blem  19056  tchcph  19186  iscfil2  19211  cfilfcls  19219  iscau4  19224  iscauf  19225  caucfil  19228  cncmet  19267  minveclem7  19328  ovoliunlem1  19390  ovolicc2lem2  19406  ovolicc2lem3  19407  ovolicc2lem4  19408  ovolicc2lem5  19409  ovolicc2  19410  voliunlem3  19438  voliun  19440  ioombl  19451  volivth  19491  ismbfd  19524  ismbf3d  19538  itg1addlem1  19576  i1fadd  19579  itg1addlem4  19583  itg2seq  19626  itg2split  19633  itg2monolem1  19634  itg2gt0  19644  ibllem  19648  itgvallem3  19669  iblposlem  19675  dvmptfsum  19851  rolle  19866  dvlip  19869  c1liplem1  19872  lhop1  19890  lhop2  19891  dvcvx  19896  dvfsumge  19898  dvfsumrlimge0  19906  dvfsumrlim  19907  dvfsum2  19910  mdegaddle  19989  mdegvscale  19990  mdegmullem  19993  ply1divex  20051  coeeulem  20135  plyco  20152  dgrlt  20176  vieta1  20221  ulmss  20305  ulmdvlem3  20310  iblulm  20315  tanord  20432  eff1olem  20442  logdivlt  20508  logccv  20546  lawcos  20650  leibpilem1  20772  xrlimcnp  20799  cxp2limlem  20806  cxp2lim  20807  cxploglim2  20809  divsqrsumo1  20814  ftalem2  20848  sqff1o  20957  dvdsppwf1o  20963  dvdsflf1o  20964  musum  20968  muinv  20970  fsumdvdsmul  20972  sgmmul  20977  fsumvma  20989  logfac2  20993  chpchtsum  20995  logfacrlim  21000  logexprlim  21001  dchrelbas3  21014  dchrmulcl  21025  bposlem1  21060  lgsdchr  21124  lgsquadlem1  21130  lgsquadlem2  21131  lgsquad2lem2  21135  chebbnd1lem1  21155  chpchtlim  21165  rplogsumlem2  21171  dchrmusum2  21180  dchrvmasumlem1  21181  dchrvmasum2lem  21182  dchrvmasumlem2  21184  dchrvmasumlem3  21185  dchrvmasumiflem2  21188  dchrisum0flb  21196  dchrisum0fno1  21197  rpvmasum2  21198  dchrisum0re  21199  dchrisum0lem1  21202  dchrisum0lem2a  21203  dchrisum0lem2  21204  dchrisum0lem3  21205  rplogsum  21213  mulogsum  21218  mulog2sumlem2  21221  vmalogdivsum2  21224  2vmadivsumlem  21226  selberglem2  21232  selberg3lem1  21243  selberg4lem1  21246  selberg4  21247  pntrsumo1  21251  selberg34r  21257  pntrlog2bndlem1  21263  pntrlog2bndlem2  21264  pntrlog2bndlem3  21265  pntrlog2bndlem4  21266  pntrlog2bndlem5  21267  pntrlog2bndlem6  21269  pntibndlem3  21278  pntlemp  21296  ostthlem1  21313  ostth3  21324  usgrasscusgra  21484  grpoidinv  21788  grporcan  21801  grpoinvid1  21810  grpoinvid2  21811  grpolcan  21813  isgrp2d  21815  gxadd  21855  ablo4  21867  ghgrp  21948  nvsubadd  22128  nvabs  22154  sspph  22348  minvecolem7  22377  htthlem  22412  hvadd4  22530  hvaddsub4  22572  shscli  22811  pjspansn  23071  fh1  23112  fh2  23113  cm2j  23114  chscllem2  23132  spansncvi  23146  5oalem2  23149  5oalem5  23152  5oalem6  23153  3oalem2  23157  hoadd4  23279  cnvunop  23413  bralnfn  23443  eighmorth  23459  hmops  23515  hmopm  23516  adjlnop  23581  adjmul  23587  adjadd  23588  nmopcoi  23590  kbass5  23615  kbass6  23616  hstle  23725  stlesi  23736  mdsl0  23805  mdexchi  23830  atom1d  23848  superpos  23849  cvexchlem  23863  atomli  23877  atcvatlem  23880  chirredlem2  23886  chirredlem3  23887  atcvat4i  23892  mdsymlem1  23898  mdsymlem3  23900  mdsymlem5  23902  mdsymlem6  23903  sumdmdlem  23913  sumdmdlem2  23914  cdj1i  23928  isoun  24081  indf1ofs  24415  cntmeas  24572  itgeq12dv  24633  ballotlemfc0  24742  ballotlemfcc  24743  lgambdd  24813  derangenlem  24849  subfacp1lem3  24860  subfacp1lem5  24862  cvmliftmolem2  24961  cvmliftlem6  24969  cvmlift2lem5  24986  cvmlift2lem7  24988  cvmlift2lem9  24990  relexpadd  25130  dfon2lem6  25407  wfrlem3  25532  sltres  25611  axlowdimlem15  25887  axlowdimlem16  25888  axcontlem10  25904  colinbtwnle  26044  onsuct0  26183  nndivsub  26199  supadd  26229  mblfinlem  26234  mblfinlem2  26235  mblfinlem3  26236  mbfposadd  26244  itg2addnclem3  26248  bddiblnc  26265  ftc1anclem5  26274  ftc1anclem6  26275  ftc1anclem7  26276  ftc1anc  26278  finminlem  26312  nn0prpwlem  26316  isfne  26339  isref  26350  islocfin  26367  comppfsc  26378  neibastop1  26379  neibastop2lem  26380  neibastop3  26382  tailfb  26397  frinfm  26428  filbcmb  26433  seqpo  26442  sstotbnd2  26474  isbndx  26482  ssbnd  26488  prdsbnd  26493  ismtycnv  26502  ismtyres  26508  heiborlem3  26513  heibor  26521  ghomdiv  26550  grpokerinj  26551  isdrngo2  26565  rngohomco  26581  rngoisocnv  26588  rngoisoco  26589  crngm4  26604  crngohomfo  26607  isidlc  26616  ispridl2  26639  ispridlc  26671  prtlem16  26709  ismrc  26746  eldioph2  26811  lzenom  26819  rexrabdioph  26845  fphpdo  26869  irrapxlem3  26878  elpell14qr2  26916  pell14qrreccl  26918  pell14qrdich  26923  pellfundglb  26939  monotoddzzfi  26996  2nn0ind  26999  jm2.21  27056  jm2.22  27057  dnnumch3  27113  dnwech  27114  fnwe2lem2  27117  pwssplit2  27157  pwssplit3  27158  dsmmsubg  27177  dsmmlss  27178  frlmsslsp  27216  frlmup1  27218  lindfrn  27259  f1lindf  27260  hbtlem6  27301  psgnunilem2  27386  mamuass  27428  phisum  27486  cncmpmax  27670  stoweidlem34  27750  stoweidlem48  27764  stoweidlem60  27776  otsndisj  28055  2cshw2lem1  28218  usgra2adedgspth  28268  usgra2adedgwlk  28269  usgra2adedgwlkon  28270  usgra2adedglem1  28271  frgranbnb  28347  bnj607  29224  sbcomwAUX7  29525  sbcomOLD7  29692  lubunNEW  29708  lshpcmp  29723  omllaw3  29980  omlfh1N  29993  cvratlem  30155  cvrat3  30176  cvrat4  30177  ps-2  30212  elpaddn0  30534  paddasslem10  30563  cdleme0cp  30948  cdleme32a  31175  cdlemeg49lebilem  31273  cdleme50eq  31275  tendoeq2  31508  diaglbN  31790  diameetN  31791  diainN  31792  dvhopN  31851  djaclN  31871  djajN  31872  dihopelvalcpre  31983  dih1dimatlem  32064  dihmeetcl  32080  djhcl  32135  mapdpglem2  32408
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