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

Theorem adantrr 697
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 443 . 2  |-  ( ( ps  /\  th )  ->  ps )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan2 460 1  |-  ( (
ph  /\  ( ps  /\ 
th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  ad2ant2r  727  ad2ant2lr  728  consensus  925  3ad2antr1  1120  sbcom  2029  ax11eq  2132  ax11el  2133  po2nr  4327  sotric  4340  sotrieq  4341  tz7.7  4418  ordsucun  4616  fcof1o  5803  isocnv  5827  isores2  5830  isomin  5834  isoini  5835  f1oiso2  5849  ovmpt2df  5979  offval  6085  xp1st  6149  1stconst  6207  cnvf1olem  6216  fnse  6232  oalim  6531  omlim  6532  oaass  6559  omordi  6564  omwordri  6570  odi  6577  oen0  6584  oewordri  6590  nnawordi  6619  nnmordi  6629  omabs  6645  erinxp  6733  dom2lem  6901  mapen  7025  ssenen  7035  ssfi  7083  domfi  7084  domunfican  7129  ordtypelem6  7238  ordtypelem7  7239  card2inf  7269  inf3lem6  7334  cantnfle  7372  cantnflem1b  7388  cantnflem1  7391  mapfien  7399  wemapwe  7400  rankxplim3  7551  fseqenlem2  7652  dfac5lem4  7753  dfac2  7757  cfsuc  7883  cfflb  7885  cofsmo  7895  infpssrlem4  7932  fin4en1  7935  ssfin4  7936  fin23lem26  7951  fin23lem22  7953  fin23lem27  7954  isf34lem4  8003  isf34lem5  8004  fin1a2lem12  8037  axdc3lem2  8077  axdc4lem  8081  ttukeylem6  8141  iundom2g  8162  pwcfsdom  8205  gchen2  8248  gchor  8249  fpwwe2lem7  8258  fpwwe2lem9  8260  fpwwe2lem11  8262  fpwwe2lem12  8263  fpwwe2  8265  pwfseqlem4  8284  gchina  8321  ltexprlem6  8665  prlem936  8671  mul4  8981  2addsub  9065  muladd  9212  ltleadd  9257  leord1  9300  eqord1  9301  ltord2  9302  leord2  9303  eqord2  9304  divmul3  9429  divcan7  9469  divadddiv  9475  lemul2a  9611  lemul12b  9613  ltmuldiv2  9627  ltdivmul  9628  ledivmul  9629  ltdivmul2  9631  lt2mul2div  9632  ledivmul2  9633  lemuldiv2  9636  lt2msq  9640  ltdiv23  9647  lediv23  9648  supmullem1  9720  infmrcl  9733  cju  9742  zextlt  10086  suprzcl  10091  zmax  10313  xrlttr  10474  xrre3  10500  qbtwnre  10526  xrsupsslem  10625  xrinfmsslem  10626  supxrunb1  10638  supxrunb2  10639  ixxdisj  10671  iooshf  10728  icodisj  10761  iccf1o  10778  modid  10993  modadd1  11001  modmul1  11002  seqf1o  11087  expsub  11149  sqlecan  11209  bcval5  11330  hashmap  11387  hashfacen  11392  seqcoll  11401  resqreu  11738  lenegsq  11804  limsupbnd2  11957  icco1  12014  rlimresb  12039  rlimsqzlem  12122  rlimsqz  12123  rlimsqz2  12124  caucvgrlem  12145  fsum0diag2  12245  o1fsum  12271  incexclem  12295  ruclem8  12515  dvdsmulcr  12558  ndvdsadd  12607  bitsshft  12666  hashdvds  12843  eulerthlem2  12850  pcqmul  12906  pcmpt  12940  prmreclem3  12965  4sqlem11  13002  0ram  13067  ramub1  13075  invfun  13666  coaval  13900  catcisolem  13938  prfcl  13977  prf1st  13978  prf2nd  13979  1st2ndprf  13980  evlfcl  13996  curfuncf  14012  curf2ndf  14021  isposd  14089  lubun  14227  isacs3lem  14269  pslem  14315  psss  14323  spwpr4  14340  pwsdiagmhm  14445  gsumccat  14464  grpinvid1  14530  grpinvid2  14531  grplcan  14534  grplactcnv  14564  0nsg  14662  eqger  14667  resghm  14699  conjghm  14713  subgga  14754  gaorber  14762  gastacl  14763  orbsta  14767  odid  14853  odmulg  14869  gexid  14892  odcau  14915  lsmssv  14954  lsmcom2  14966  pj1ghm  15012  frgpuptf  15079  frgpup1  15084  ghmplusg  15138  cyggex2  15183  gsumval3eu  15190  gsumval3  15191  ablfac1eu  15308  pgpfac1lem5  15314  isdrngd  15537  issrngd  15626  lmhmf1o  15803  lmhmima  15804  lmhmpreima  15805  lspextmo  15813  lspdisj  15878  islbs3  15908  lbsextlem4  15914  drngnidl  15981  lidldvgen  16007  issubassa2  16084  psrbagconf1o  16120  evlslem2  16249  ply1sclf1  16364  cnsubrg  16432  znunit  16517  cygznlem3  16523  eltg2  16696  ntrss  16792  opncldf1  16821  ssnei2  16853  neindisj  16854  restopnb  16906  restntr  16912  tgcmp  17128  hauscmplem  17133  2ndc1stc  17177  2ndcdisj  17182  2ndcomap  17184  restlly  17209  lly1stc  17222  txcls  17299  txdis1cn  17329  pthaus  17332  txlm  17342  qtoptop2  17390  qtopomap  17409  kqt0lem  17427  pt1hmeo  17497  ptuncnv  17498  xkocnv  17505  fbasfip  17563  fgabs  17574  fbasrn  17579  elfm2  17643  fmfnfmlem2  17650  fmfnfmlem4  17652  ptcmplem3  17748  ptcmplem4  17749  tsmsres  17826  tsmsxplem1  17835  elbl2  17950  blin  17970  xmeter  17979  xmetresbl  17983  stdbdxmet  18061  metrest  18070  dscmet  18095  nrmmetd  18097  tngngp2  18168  nmoi2  18239  icccmplem2  18328  reconnlem2  18332  metdstri  18355  metdsle  18356  metdsre  18357  metnrmlem3  18365  fsumcn  18374  icccvx  18448  bndth  18456  evth  18457  reparphti  18495  pi1blem  18537  tchcph  18667  iscfil2  18692  cfilfcls  18700  iscau4  18705  iscauf  18706  caucfil  18709  cncmet  18744  minveclem7  18799  ovoliunlem1  18861  ovolicc2lem2  18877  ovolicc2lem3  18878  ovolicc2lem4  18879  ovolicc2lem5  18880  ovolicc2  18881  voliunlem3  18909  voliun  18911  ioombl  18922  volivth  18962  ismbfd  18995  ismbf3d  19009  itg1addlem1  19047  i1fadd  19050  itg1addlem4  19054  itg2seq  19097  itg2split  19104  itg2monolem1  19105  itg2gt0  19115  ibllem  19119  itgvallem3  19140  iblposlem  19146  dvmptfsum  19322  rolle  19337  dvlip  19340  c1liplem1  19343  lhop1  19361  lhop2  19362  dvcvx  19367  dvfsumge  19369  dvfsumrlimge0  19377  dvfsumrlim  19378  dvfsum2  19381  mdegaddle  19460  mdegvscale  19461  mdegmullem  19464  ply1divex  19522  coeeulem  19606  plyco  19623  dgrlt  19647  vieta1  19692  ulmss  19774  ulmdvlem3  19779  iblulm  19783  tanord  19900  eff1olem  19910  logdivlt  19972  logccv  20010  lawcos  20114  leibpilem1  20236  xrlimcnp  20263  cxp2limlem  20270  cxp2lim  20271  cxploglim2  20273  divsqrsumo1  20278  ftalem2  20311  sqff1o  20420  dvdsppwf1o  20426  dvdsflf1o  20427  musum  20431  muinv  20433  fsumdvdsmul  20435  sgmmul  20440  fsumvma  20452  logfac2  20456  chpchtsum  20458  logfacrlim  20463  logexprlim  20464  dchrelbas3  20477  dchrmulcl  20488  bposlem1  20523  lgsdchr  20587  lgsquadlem1  20593  lgsquadlem2  20594  lgsquad2lem2  20598  chebbnd1lem1  20618  chpchtlim  20628  rplogsumlem2  20634  dchrmusum2  20643  dchrvmasumlem1  20644  dchrvmasum2lem  20645  dchrvmasumlem2  20647  dchrvmasumlem3  20648  dchrvmasumiflem2  20651  dchrisum0flb  20659  dchrisum0fno1  20660  rpvmasum2  20661  dchrisum0re  20662  dchrisum0lem1  20665  dchrisum0lem2a  20666  dchrisum0lem2  20667  dchrisum0lem3  20668  rplogsum  20676  mulogsum  20681  mulog2sumlem2  20684  vmalogdivsum2  20687  2vmadivsumlem  20689  selberglem2  20695  selberg3lem1  20706  selberg4lem1  20709  selberg4  20710  pntrsumo1  20714  selberg34r  20720  pntrlog2bndlem1  20726  pntrlog2bndlem2  20727  pntrlog2bndlem3  20728  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntrlog2bndlem6  20732  pntibndlem3  20741  pntlemp  20759  ostthlem1  20776  ostth3  20787  grpoidinv  20875  grporcan  20888  grpoinvid1  20897  grpoinvid2  20898  grpolcan  20900  isgrp2d  20902  gxadd  20942  ablo4  20954  ghgrp  21035  nvsubadd  21213  nvabs  21239  sspph  21433  minvecolem7  21462  htthlem  21497  hvadd4  21615  hvaddsub4  21657  shscli  21896  pjspansn  22156  fh1  22197  fh2  22198  cm2j  22199  chscllem2  22217  spansncvi  22231  5oalem2  22234  5oalem5  22237  5oalem6  22238  3oalem2  22242  hoadd4  22364  cnvunop  22498  bralnfn  22528  eighmorth  22544  hmops  22600  hmopm  22601  adjlnop  22666  adjmul  22672  adjadd  22673  nmopcoi  22675  kbass5  22700  kbass6  22701  hstle  22810  stlesi  22821  mdsl0  22890  mdexchi  22915  atom1d  22933  superpos  22934  cvexchlem  22948  atomli  22962  atcvatlem  22965  chirredlem2  22971  chirredlem3  22972  atcvat4i  22977  mdsymlem1  22983  mdsymlem3  22985  mdsymlem5  22987  mdsymlem6  22988  sumdmdlem  22998  sumdmdlem2  22999  cdj1i  23013  ballotlemfc0  23051  ballotlemfcc  23052  itgeq12dv  23196  isoun  23242  xrre3FL  23251  cntmeas  23553  indf1ofs  23609  derangenlem  23702  subfacp1lem3  23713  subfacp1lem5  23715  cvmliftmolem2  23813  cvmliftlem6  23821  cvmlift2lem5  23838  cvmlift2lem7  23840  cvmlift2lem9  23842  relexpadd  24035  dfon2lem6  24144  wfrlem3  24258  sltres  24318  axlowdimlem15  24584  axlowdimlem16  24585  axcontlem10  24601  colinbtwnle  24741  onsuct0  24880  nndivsub  24896  dfoprab4pop  25037  npincppr  25159  preotr2  25235  fprodadd  25352  gapm2  25369  mulinvsca  25480  truni3  25507  limptlimpr  25576  mulmulvec  25687  iepiclem  25823  cmp2morp  25958  rocatval  25959  finminlem  26231  nn0prpwlem  26238  isfne  26268  isref  26279  islocfin  26296  comppfsc  26307  neibastop1  26308  neibastop2lem  26309  neibastop3  26311  tailfb  26326  frinfm  26416  filbcmb  26432  seqpo  26457  sstotbnd2  26498  isbndx  26506  ssbnd  26512  prdsbnd  26517  ismtycnv  26526  ismtyres  26532  heiborlem3  26537  heibor  26545  ghomdiv  26574  grpokerinj  26575  isdrngo2  26589  rngohomco  26605  rngoisocnv  26612  rngoisoco  26613  crngm4  26628  crngohomfo  26631  isidlc  26640  ispridl2  26663  ispridlc  26695  prtlem16  26737  ismrc  26776  eldioph2  26841  lzenom  26849  rexrabdioph  26875  fphpdo  26900  irrapxlem3  26909  elpell14qr2  26947  pell14qrreccl  26949  pell14qrdich  26954  pellfundglb  26970  monotoddzzfi  27027  2nn0ind  27030  jm2.21  27087  jm2.22  27088  dnnumch3  27144  dnwech  27145  fnwe2lem2  27148  pwssplit2  27189  pwssplit3  27190  dsmmsubg  27209  dsmmlss  27210  frlmsslsp  27248  frlmup1  27250  lindfrn  27291  f1lindf  27292  hbtlem6  27333  psgnunilem2  27418  mamuass  27460  phisum  27518  stoweidlem34  27783  stoweidlem48  27797  mpt2xopoveq  28085  bnj607  28948  lubunNEW  29163  lshpcmp  29178  omllaw3  29435  omlfh1N  29448  cvratlem  29610  cvrat3  29631  cvrat4  29632  ps-2  29667  elpaddn0  29989  paddasslem10  30018  cdleme0cp  30403  cdleme32a  30630  cdlemeg49lebilem  30728  cdleme50eq  30730  tendoeq2  30963  diaglbN  31245  diameetN  31246  diainN  31247  dvhopN  31306  djaclN  31326  djajN  31327  dihopelvalcpre  31438  dih1dimatlem  31519  dihmeetcl  31535  djhcl  31590  mapdpglem2  31863
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 177  df-an 360
  Copyright terms: Public domain W3C validator