MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adantrr 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  2138  ax11eq  2243  ax11el  2244  po2nr  4476  sotric  4489  sotrieq  4490  tz7.7  4567  ordsucun  4764  fvtp1g  5901  fcof1o  5985  isocnv  6009  isores2  6012  isomin  6016  isoini  6017  f1oiso2  6031  ovmpt2df  6164  offval  6271  xp1st  6335  1stconst  6394  cnvf1olem  6403  fnse  6422  mpt2xopoveq  6429  oalim  6735  omlim  6736  oaass  6763  omordi  6768  omwordri  6774  odi  6781  oen0  6788  oewordri  6794  nnawordi  6823  nnmordi  6833  omabs  6849  erinxp  6937  dom2lem  7106  mapen  7230  ssenen  7240  ssfi  7288  domfi  7289  domunfican  7338  ordtypelem6  7448  ordtypelem7  7449  card2inf  7479  inf3lem6  7544  cantnfle  7582  cantnflem1b  7598  cantnflem1  7601  mapfien  7609  wemapwe  7610  rankxplim3  7761  fseqenlem2  7862  dfac5lem4  7963  dfac2  7967  cfsuc  8093  cfflb  8095  cofsmo  8105  infpssrlem4  8142  fin4en1  8145  ssfin4  8146  fin23lem26  8161  fin23lem22  8163  fin23lem27  8164  isf34lem4  8213  isf34lem5  8214  fin1a2lem12  8247  axdc3lem2  8287  axdc4lem  8291  ttukeylem6  8350  iundom2g  8371  pwcfsdom  8414  gchen2  8457  gchor  8458  fpwwe2lem7  8467  fpwwe2lem9  8469  fpwwe2lem11  8471  fpwwe2lem12  8472  fpwwe2  8474  pwfseqlem4  8493  gchina  8530  ltexprlem6  8874  prlem936  8880  mul4  9191  2addsub  9275  muladd  9422  ltleadd  9467  leord1  9510  eqord1  9511  ltord2  9512  leord2  9513  eqord2  9514  divmul3  9639  divcan7  9679  divadddiv  9685  lemul2a  9821  lemul12b  9823  ltmuldiv2  9837  ltdivmul  9838  ledivmul  9839  ltdivmul2  9841  lt2mul2div  9842  ledivmul2  9843  lemuldiv2  9846  lt2msq  9850  ltdiv23  9857  lediv23  9858  supmullem1  9930  infmrcl  9943  cju  9952  zextlt  10300  suprzcl  10305  zmax  10527  xrlttr  10689  xrre3  10715  qbtwnre  10741  xrsupsslem  10841  xrinfmsslem  10842  supxrunb1  10854  supxrunb2  10855  ixxdisj  10887  iooshf  10945  icodisj  10978  iccf1o  10995  modid  11225  modadd1  11233  modmul1  11234  seqf1o  11319  expsub  11382  sqlecan  11442  bcval5  11564  hashmap  11653  hashfacen  11658  seqcoll  11667  resqreu  12013  lenegsq  12079  limsupbnd2  12232  icco1  12289  rlimresb  12314  rlimsqzlem  12397  rlimsqz  12398  rlimsqz2  12399  caucvgrlem  12421  fsum0diag2  12521  o1fsum  12547  ruclem8  12791  dvdsmulcr  12834  ndvdsadd  12883  bitsshft  12942  hashdvds  13119  eulerthlem2  13126  pcqmul  13182  pcmpt  13216  prmreclem3  13241  4sqlem11  13278  0ram  13343  ramub1  13351  invfun  13944  coaval  14178  catcisolem  14216  prfcl  14255  prf1st  14256  prf2nd  14257  1st2ndprf  14258  curfuncf  14290  isposd  14367  lubun  14505  isacs3lem  14547  pslem  14593  psss  14601  spwpr4  14618  pwsdiagmhm  14723  gsumccat  14742  grpinvid1  14808  grpinvid2  14809  grplcan  14812  grplactcnv  14842  0nsg  14940  eqger  14945  resghm  14977  conjghm  14991  subgga  15032  gaorber  15040  gastacl  15041  orbsta  15045  odid  15131  odmulg  15147  gexid  15170  odcau  15193  lsmssv  15232  lsmcom2  15244  pj1ghm  15290  frgpuptf  15357  frgpup1  15362  ghmplusg  15416  cyggex2  15461  gsumval3eu  15468  gsumval3  15469  ablfac1eu  15586  pgpfac1lem5  15592  isdrngd  15815  issrngd  15904  lmhmf1o  16077  lmhmima  16078  lmhmpreima  16079  lspextmo  16087  lspdisj  16152  islbs3  16182  lbsextlem4  16188  drngnidl  16255  lidldvgen  16281  issubassa2  16358  psrbagconf1o  16394  evlslem2  16523  ply1sclf1  16635  cnsubrg  16714  znunit  16799  cygznlem3  16805  eltg2  16978  ntrss  17074  opncldf1  17103  ssnei2  17135  neindisj  17136  restopnb  17193  restntr  17200  tgcmp  17418  hauscmplem  17423  2ndc1stc  17467  2ndcdisj  17472  2ndcomap  17474  restlly  17499  lly1stc  17512  txcls  17589  txdis1cn  17620  pthaus  17623  txlm  17633  qtoptop2  17684  qtopomap  17703  kqt0lem  17721  pt1hmeo  17791  ptuncnv  17792  xkocnv  17799  fbasfip  17853  fgabs  17864  fbasrn  17869  elfm2  17933  fmfnfmlem2  17940  fmfnfmlem4  17942  ptcmplem3  18038  ptcmplem4  18039  tsmsres  18126  tsmsxplem1  18135  utoptop  18217  elbl2ps  18372  elbl2  18373  blin  18404  xmeter  18416  xmetresbl  18420  stdbdxmet  18498  metrest  18507  metustexhalfOLD  18546  metustexhalf  18547  dscmet  18573  nrmmetd  18575  tngngp2  18646  nmoi2  18717  icccmplem2  18807  reconnlem2  18811  metdstri  18834  metdsle  18835  metdsre  18836  metnrmlem3  18844  fsumcn  18853  icccvx  18928  bndth  18936  evth  18937  reparphti  18975  pi1blem  19017  tchcph  19147  iscfil2  19172  cfilfcls  19180  iscau4  19185  iscauf  19186  caucfil  19189  cncmet  19228  minveclem7  19289  ovoliunlem1  19351  ovolicc2lem2  19367  ovolicc2lem3  19368  ovolicc2lem4  19369  ovolicc2lem5  19370  ovolicc2  19371  voliunlem3  19399  voliun  19401  ioombl  19412  volivth  19452  ismbfd  19485  ismbf3d  19499  itg1addlem1  19537  i1fadd  19540  itg1addlem4  19544  itg2seq  19587  itg2split  19594  itg2monolem1  19595  itg2gt0  19605  ibllem  19609  itgvallem3  19630  iblposlem  19636  dvmptfsum  19812  rolle  19827  dvlip  19830  c1liplem1  19833  lhop1  19851  lhop2  19852  dvcvx  19857  dvfsumge  19859  dvfsumrlimge0  19867  dvfsumrlim  19868  dvfsum2  19871  mdegaddle  19950  mdegvscale  19951  mdegmullem  19954  ply1divex  20012  coeeulem  20096  plyco  20113  dgrlt  20137  vieta1  20182  ulmss  20266  ulmdvlem3  20271  iblulm  20276  tanord  20393  eff1olem  20403  logdivlt  20469  logccv  20507  lawcos  20611  leibpilem1  20733  xrlimcnp  20760  cxp2limlem  20767  cxp2lim  20768  cxploglim2  20770  divsqrsumo1  20775  ftalem2  20809  sqff1o  20918  dvdsppwf1o  20924  dvdsflf1o  20925  musum  20929  muinv  20931  fsumdvdsmul  20933  sgmmul  20938  fsumvma  20950  logfac2  20954  chpchtsum  20956  logfacrlim  20961  logexprlim  20962  dchrelbas3  20975  dchrmulcl  20986  bposlem1  21021  lgsdchr  21085  lgsquadlem1  21091  lgsquadlem2  21092  lgsquad2lem2  21096  chebbnd1lem1  21116  chpchtlim  21126  rplogsumlem2  21132  dchrmusum2  21141  dchrvmasumlem1  21142  dchrvmasum2lem  21143  dchrvmasumlem2  21145  dchrvmasumlem3  21146  dchrvmasumiflem2  21149  dchrisum0flb  21157  dchrisum0fno1  21158  rpvmasum2  21159  dchrisum0re  21160  dchrisum0lem1  21163  dchrisum0lem2a  21164  dchrisum0lem2  21165  dchrisum0lem3  21166  rplogsum  21174  mulogsum  21179  mulog2sumlem2  21182  vmalogdivsum2  21185  2vmadivsumlem  21187  selberglem2  21193  selberg3lem1  21204  selberg4lem1  21207  selberg4  21208  pntrsumo1  21212  selberg34r  21218  pntrlog2bndlem1  21224  pntrlog2bndlem2  21225  pntrlog2bndlem3  21226  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntrlog2bndlem6  21230  pntibndlem3  21239  pntlemp  21257  ostthlem1  21274  ostth3  21285  usgrasscusgra  21445  grpoidinv  21749  grporcan  21762  grpoinvid1  21771  grpoinvid2  21772  grpolcan  21774  isgrp2d  21776  gxadd  21816  ablo4  21828  ghgrp  21909  nvsubadd  22089  nvabs  22115  sspph  22309  minvecolem7  22338  htthlem  22373  hvadd4  22491  hvaddsub4  22533  shscli  22772  pjspansn  23032  fh1  23073  fh2  23074  cm2j  23075  chscllem2  23093  spansncvi  23107  5oalem2  23110  5oalem5  23113  5oalem6  23114  3oalem2  23118  hoadd4  23240  cnvunop  23374  bralnfn  23404  eighmorth  23420  hmops  23476  hmopm  23477  adjlnop  23542  adjmul  23548  adjadd  23549  nmopcoi  23551  kbass5  23576  kbass6  23577  hstle  23686  stlesi  23697  mdsl0  23766  mdexchi  23791  atom1d  23809  superpos  23810  cvexchlem  23824  atomli  23838  atcvatlem  23841  chirredlem2  23847  chirredlem3  23848  atcvat4i  23853  mdsymlem1  23859  mdsymlem3  23861  mdsymlem5  23863  mdsymlem6  23864  sumdmdlem  23874  sumdmdlem2  23875  cdj1i  23889  isoun  24042  indf1ofs  24376  cntmeas  24533  itgeq12dv  24594  ballotlemfc0  24703  ballotlemfcc  24704  lgambdd  24774  derangenlem  24810  subfacp1lem3  24821  subfacp1lem5  24823  cvmliftmolem2  24922  cvmliftlem6  24930  cvmlift2lem5  24947  cvmlift2lem7  24949  cvmlift2lem9  24951  relexpadd  25091  dfon2lem6  25358  wfrlem3  25472  sltres  25532  axlowdimlem15  25799  axlowdimlem16  25800  axcontlem10  25816  colinbtwnle  25956  onsuct0  26095  nndivsub  26111  supadd  26138  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  mbfposadd  26153  itg2addnclem3  26157  bddiblnc  26174  finminlem  26211  nn0prpwlem  26215  isfne  26238  isref  26249  islocfin  26266  comppfsc  26277  neibastop1  26278  neibastop2lem  26279  neibastop3  26281  tailfb  26296  frinfm  26327  filbcmb  26332  seqpo  26341  sstotbnd2  26373  isbndx  26381  ssbnd  26387  prdsbnd  26392  ismtycnv  26401  ismtyres  26407  heiborlem3  26412  heibor  26420  ghomdiv  26449  grpokerinj  26450  isdrngo2  26464  rngohomco  26480  rngoisocnv  26487  rngoisoco  26488  crngm4  26503  crngohomfo  26506  isidlc  26515  ispridl2  26538  ispridlc  26570  prtlem16  26608  ismrc  26645  eldioph2  26710  lzenom  26718  rexrabdioph  26744  fphpdo  26768  irrapxlem3  26777  elpell14qr2  26815  pell14qrreccl  26817  pell14qrdich  26822  pellfundglb  26838  monotoddzzfi  26895  2nn0ind  26898  jm2.21  26955  jm2.22  26956  dnnumch3  27012  dnwech  27013  fnwe2lem2  27016  pwssplit2  27057  pwssplit3  27058  dsmmsubg  27077  dsmmlss  27078  frlmsslsp  27116  frlmup1  27118  lindfrn  27159  f1lindf  27160  hbtlem6  27201  psgnunilem2  27286  mamuass  27328  phisum  27386  cncmpmax  27570  stoweidlem34  27650  stoweidlem48  27664  stoweidlem60  27676  otsndisj  27953  usgra2adedgspth  28045  usgra2adedgwlk  28046  usgra2adedgwlkon  28047  usgra2adedglem1  28048  frgranbnb  28124  bnj607  28993  sbcomwAUX7  29291  sbcomOLD7  29439  lubunNEW  29456  lshpcmp  29471  omllaw3  29728  omlfh1N  29741  cvratlem  29903  cvrat3  29924  cvrat4  29925  ps-2  29960  elpaddn0  30282  paddasslem10  30311  cdleme0cp  30696  cdleme32a  30923  cdlemeg49lebilem  31021  cdleme50eq  31023  tendoeq2  31256  diaglbN  31538  diameetN  31539  diainN  31540  dvhopN  31599  djaclN  31619  djajN  31620  dihopelvalcpre  31731  dih1dimatlem  31812  dihmeetcl  31828  djhcl  31883  mapdpglem2  32156
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