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  2164  ax11eq  2269  ax11el  2270  po2nr  4508  sotric  4521  sotrieq  4522  tz7.7  4599  ordsucun  4796  fvtp1g  5933  fcof1o  6017  isocnv  6041  isores2  6044  isomin  6048  isoini  6049  f1oiso2  6063  ovmpt2df  6196  offval  6303  xp1st  6367  1stconst  6426  cnvf1olem  6435  fnse  6454  mpt2xopoveq  6461  oalim  6767  omlim  6768  oaass  6795  omordi  6800  omwordri  6806  odi  6813  oen0  6820  oewordri  6826  nnawordi  6855  nnmordi  6865  omabs  6881  erinxp  6969  dom2lem  7138  mapen  7262  ssenen  7272  ssfi  7320  domfi  7321  domunfican  7370  ordtypelem6  7481  ordtypelem7  7482  card2inf  7512  inf3lem6  7577  cantnfle  7615  cantnflem1b  7631  cantnflem1  7634  mapfien  7642  wemapwe  7643  rankxplim3  7794  fseqenlem2  7895  dfac5lem4  7996  dfac2  8000  cfsuc  8126  cfflb  8128  cofsmo  8138  infpssrlem4  8175  fin4en1  8178  ssfin4  8179  fin23lem26  8194  fin23lem22  8196  fin23lem27  8197  isf34lem4  8246  isf34lem5  8247  fin1a2lem12  8280  axdc3lem2  8320  axdc4lem  8324  ttukeylem6  8383  iundom2g  8404  pwcfsdom  8447  gchen2  8490  gchor  8491  fpwwe2lem7  8500  fpwwe2lem9  8502  fpwwe2lem11  8504  fpwwe2lem12  8505  fpwwe2  8507  pwfseqlem4  8526  gchina  8563  ltexprlem6  8907  prlem936  8913  mul4  9224  2addsub  9308  muladd  9455  ltleadd  9500  leord1  9543  eqord1  9544  ltord2  9545  leord2  9546  eqord2  9547  divmul3  9672  divcan7  9712  divadddiv  9718  lemul2a  9854  lemul12b  9856  ltmuldiv2  9870  ltdivmul  9871  ledivmul  9872  ltdivmul2  9874  lt2mul2div  9875  ledivmul2  9876  lemuldiv2  9879  lt2msq  9883  ltdiv23  9890  lediv23  9891  supmullem1  9963  infmrcl  9976  cju  9985  zextlt  10333  suprzcl  10338  zmax  10560  xrlttr  10722  xrre3  10748  qbtwnre  10774  xrsupsslem  10874  xrinfmsslem  10875  supxrunb1  10887  supxrunb2  10888  ixxdisj  10920  iooshf  10978  icodisj  11011  iccf1o  11028  modid  11258  modadd1  11266  modmul1  11267  seqf1o  11352  expsub  11415  sqlecan  11475  bcval5  11597  hashmap  11686  hashfacen  11691  seqcoll  11700  resqreu  12046  lenegsq  12112  limsupbnd2  12265  icco1  12322  rlimresb  12347  rlimsqzlem  12430  rlimsqz  12431  rlimsqz2  12432  caucvgrlem  12454  fsum0diag2  12554  o1fsum  12580  ruclem8  12824  dvdsmulcr  12867  ndvdsadd  12916  bitsshft  12975  hashdvds  13152  eulerthlem2  13159  pcqmul  13215  pcmpt  13249  prmreclem3  13274  4sqlem11  13311  0ram  13376  ramub1  13384  invfun  13977  coaval  14211  catcisolem  14249  prfcl  14288  prf1st  14289  prf2nd  14290  1st2ndprf  14291  curfuncf  14323  isposd  14400  lubun  14538  isacs3lem  14580  pslem  14626  psss  14634  spwpr4  14651  pwsdiagmhm  14756  gsumccat  14775  grpinvid1  14841  grpinvid2  14842  grplcan  14845  grplactcnv  14875  0nsg  14973  eqger  14978  resghm  15010  conjghm  15024  subgga  15065  gaorber  15073  gastacl  15074  orbsta  15078  odid  15164  odmulg  15180  gexid  15203  odcau  15226  lsmssv  15265  lsmcom2  15277  pj1ghm  15323  frgpuptf  15390  frgpup1  15395  ghmplusg  15449  cyggex2  15494  gsumval3eu  15501  gsumval3  15502  ablfac1eu  15619  pgpfac1lem5  15625  isdrngd  15848  issrngd  15937  lmhmf1o  16110  lmhmima  16111  lmhmpreima  16112  lspextmo  16120  lspdisj  16185  islbs3  16215  lbsextlem4  16221  drngnidl  16288  lidldvgen  16314  issubassa2  16391  psrbagconf1o  16427  evlslem2  16556  ply1sclf1  16668  cnsubrg  16747  znunit  16832  cygznlem3  16838  eltg2  17011  ntrss  17107  opncldf1  17136  ssnei2  17168  neindisj  17169  restopnb  17227  restntr  17234  tgcmp  17452  hauscmplem  17457  2ndc1stc  17502  2ndcdisj  17507  2ndcomap  17509  restlly  17534  lly1stc  17547  txcls  17624  txdis1cn  17655  pthaus  17658  txlm  17668  qtoptop2  17719  qtopomap  17738  kqt0lem  17756  pt1hmeo  17826  ptuncnv  17827  xkocnv  17834  fbasfip  17888  fgabs  17899  fbasrn  17904  elfm2  17968  fmfnfmlem2  17975  fmfnfmlem4  17977  ptcmplem3  18073  ptcmplem4  18074  tsmsres  18161  tsmsxplem1  18170  utoptop  18252  elbl2ps  18407  elbl2  18408  blin  18439  xmeter  18451  xmetresbl  18455  stdbdxmet  18533  metrest  18542  metustexhalfOLD  18581  metustexhalf  18582  dscmet  18608  nrmmetd  18610  tngngp2  18681  nmoi2  18752  icccmplem2  18842  reconnlem2  18846  metdstri  18869  metdsle  18870  metdsre  18871  metnrmlem3  18879  fsumcn  18888  icccvx  18963  bndth  18971  evth  18972  reparphti  19010  pi1blem  19052  tchcph  19182  iscfil2  19207  cfilfcls  19215  iscau4  19220  iscauf  19221  caucfil  19224  cncmet  19263  minveclem7  19324  ovoliunlem1  19386  ovolicc2lem2  19402  ovolicc2lem3  19403  ovolicc2lem4  19404  ovolicc2lem5  19405  ovolicc2  19406  voliunlem3  19434  voliun  19436  ioombl  19447  volivth  19487  ismbfd  19520  ismbf3d  19534  itg1addlem1  19572  i1fadd  19575  itg1addlem4  19579  itg2seq  19622  itg2split  19629  itg2monolem1  19630  itg2gt0  19640  ibllem  19644  itgvallem3  19665  iblposlem  19671  dvmptfsum  19847  rolle  19862  dvlip  19865  c1liplem1  19868  lhop1  19886  lhop2  19887  dvcvx  19892  dvfsumge  19894  dvfsumrlimge0  19902  dvfsumrlim  19903  dvfsum2  19906  mdegaddle  19985  mdegvscale  19986  mdegmullem  19989  ply1divex  20047  coeeulem  20131  plyco  20148  dgrlt  20172  vieta1  20217  ulmss  20301  ulmdvlem3  20306  iblulm  20311  tanord  20428  eff1olem  20438  logdivlt  20504  logccv  20542  lawcos  20646  leibpilem1  20768  xrlimcnp  20795  cxp2limlem  20802  cxp2lim  20803  cxploglim2  20805  divsqrsumo1  20810  ftalem2  20844  sqff1o  20953  dvdsppwf1o  20959  dvdsflf1o  20960  musum  20964  muinv  20966  fsumdvdsmul  20968  sgmmul  20973  fsumvma  20985  logfac2  20989  chpchtsum  20991  logfacrlim  20996  logexprlim  20997  dchrelbas3  21010  dchrmulcl  21021  bposlem1  21056  lgsdchr  21120  lgsquadlem1  21126  lgsquadlem2  21127  lgsquad2lem2  21131  chebbnd1lem1  21151  chpchtlim  21161  rplogsumlem2  21167  dchrmusum2  21176  dchrvmasumlem1  21177  dchrvmasum2lem  21178  dchrvmasumlem2  21180  dchrvmasumlem3  21181  dchrvmasumiflem2  21184  dchrisum0flb  21192  dchrisum0fno1  21193  rpvmasum2  21194  dchrisum0re  21195  dchrisum0lem1  21198  dchrisum0lem2a  21199  dchrisum0lem2  21200  dchrisum0lem3  21201  rplogsum  21209  mulogsum  21214  mulog2sumlem2  21217  vmalogdivsum2  21220  2vmadivsumlem  21222  selberglem2  21228  selberg3lem1  21239  selberg4lem1  21242  selberg4  21243  pntrsumo1  21247  selberg34r  21253  pntrlog2bndlem1  21259  pntrlog2bndlem2  21260  pntrlog2bndlem3  21261  pntrlog2bndlem4  21262  pntrlog2bndlem5  21263  pntrlog2bndlem6  21265  pntibndlem3  21274  pntlemp  21292  ostthlem1  21309  ostth3  21320  usgrasscusgra  21480  grpoidinv  21784  grporcan  21797  grpoinvid1  21806  grpoinvid2  21807  grpolcan  21809  isgrp2d  21811  gxadd  21851  ablo4  21863  ghgrp  21944  nvsubadd  22124  nvabs  22150  sspph  22344  minvecolem7  22373  htthlem  22408  hvadd4  22526  hvaddsub4  22568  shscli  22807  pjspansn  23067  fh1  23108  fh2  23109  cm2j  23110  chscllem2  23128  spansncvi  23142  5oalem2  23145  5oalem5  23148  5oalem6  23149  3oalem2  23153  hoadd4  23275  cnvunop  23409  bralnfn  23439  eighmorth  23455  hmops  23511  hmopm  23512  adjlnop  23577  adjmul  23583  adjadd  23584  nmopcoi  23586  kbass5  23611  kbass6  23612  hstle  23721  stlesi  23732  mdsl0  23801  mdexchi  23826  atom1d  23844  superpos  23845  cvexchlem  23859  atomli  23873  atcvatlem  23876  chirredlem2  23882  chirredlem3  23883  atcvat4i  23888  mdsymlem1  23894  mdsymlem3  23896  mdsymlem5  23898  mdsymlem6  23899  sumdmdlem  23909  sumdmdlem2  23910  cdj1i  23924  isoun  24077  indf1ofs  24411  cntmeas  24568  itgeq12dv  24629  ballotlemfc0  24738  ballotlemfcc  24739  lgambdd  24809  derangenlem  24845  subfacp1lem3  24856  subfacp1lem5  24858  cvmliftmolem2  24957  cvmliftlem6  24965  cvmlift2lem5  24982  cvmlift2lem7  24984  cvmlift2lem9  24986  relexpadd  25126  dfon2lem6  25399  wfrlem3  25513  sltres  25573  axlowdimlem15  25843  axlowdimlem16  25844  axcontlem10  25860  colinbtwnle  26000  onsuct0  26139  nndivsub  26155  supadd  26185  mblfinlem  26190  mblfinlem2  26191  mblfinlem3  26192  mbfposadd  26200  itg2addnclem3  26204  bddiblnc  26221  finminlem  26258  nn0prpwlem  26262  isfne  26285  isref  26296  islocfin  26313  comppfsc  26324  neibastop1  26325  neibastop2lem  26326  neibastop3  26328  tailfb  26343  frinfm  26374  filbcmb  26379  seqpo  26388  sstotbnd2  26420  isbndx  26428  ssbnd  26434  prdsbnd  26439  ismtycnv  26448  ismtyres  26454  heiborlem3  26459  heibor  26467  ghomdiv  26496  grpokerinj  26497  isdrngo2  26511  rngohomco  26527  rngoisocnv  26534  rngoisoco  26535  crngm4  26550  crngohomfo  26553  isidlc  26562  ispridl2  26585  ispridlc  26617  prtlem16  26655  ismrc  26692  eldioph2  26757  lzenom  26765  rexrabdioph  26791  fphpdo  26815  irrapxlem3  26824  elpell14qr2  26862  pell14qrreccl  26864  pell14qrdich  26869  pellfundglb  26885  monotoddzzfi  26942  2nn0ind  26945  jm2.21  27002  jm2.22  27003  dnnumch3  27059  dnwech  27060  fnwe2lem2  27063  pwssplit2  27104  pwssplit3  27105  dsmmsubg  27124  dsmmlss  27125  frlmsslsp  27163  frlmup1  27165  lindfrn  27206  f1lindf  27207  hbtlem6  27248  psgnunilem2  27333  mamuass  27375  phisum  27433  cncmpmax  27617  stoweidlem34  27697  stoweidlem48  27711  stoweidlem60  27723  otsndisj  28001  usgra2adedgspth  28189  usgra2adedgwlk  28190  usgra2adedgwlkon  28191  usgra2adedglem1  28192  frgranbnb  28268  bnj607  29141  sbcomwAUX7  29439  sbcomOLD7  29594  lubunNEW  29610  lshpcmp  29625  omllaw3  29882  omlfh1N  29895  cvratlem  30057  cvrat3  30078  cvrat4  30079  ps-2  30114  elpaddn0  30436  paddasslem10  30465  cdleme0cp  30850  cdleme32a  31077  cdlemeg49lebilem  31175  cdleme50eq  31177  tendoeq2  31410  diaglbN  31692  diameetN  31693  diainN  31694  dvhopN  31753  djaclN  31773  djajN  31774  dihopelvalcpre  31885  dih1dimatlem  31966  dihmeetcl  31982  djhcl  32037  mapdpglem2  32310
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