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

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

Proof of Theorem adantrl
StepHypRef Expression
1 simpr 461 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan2 474 1  |-  ( (
ph  /\  ( th  /\  ps ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  ad2ant2l  745  ad2ant2rl  748  consensus  959  cases2  971  3ad2antr2  1163  3ad2antr3  1164  ordelord  4890  foco  5795  isocnv  6211  isores2  6214  f1oiso2  6233  offval  6532  ordsucun  6645  opabex2  6723  xp2nd  6816  1stconst  6873  2ndconst  6874  smoord  7038  tfrlem9  7056  tfrlem11  7059  oaass  7212  omordi  7217  omwordri  7223  odi  7230  oewordri  7243  nnawordi  7272  nnmordi  7282  dom2lem  7557  fundmen  7591  sbthlem9  7637  mapen  7683  mapunen  7688  ssenen  7693  domfi  7743  mapfien  7869  inf3lem6  8053  mapfienOLD  8141  r1val1  8207  rankval3b  8247  numacn  8433  infxpabs  8595  infxp  8598  cfsmolem  8653  infpssrlem4  8689  fin23lem27  8711  isf34lem4  8760  hsmexlem2  8810  axdc3lem2  8834  axdc3lem4  8836  iundom2g  8918  gchen1  9006  fpwwe2lem7  9017  fpwwe2lem11  9021  fpwwe2lem12  9022  prlem936  9428  muladd  9996  leord1  10087  eqord1  10088  ltord2  10089  leord2  10090  eqord2  10091  divadddiv  10266  ltmul12a  10405  lemul12b  10406  supmullem1  10516  cju  10539  zextlt  10944  zmax  11190  xrre  11381  supxr  11515  ixxdisj  11555  iooshf  11614  icodisj  11656  ioojoin  11662  iccshftr  11665  iccshftl  11667  iccdil  11669  icccntr  11671  iccf1o  11675  fzaddel  11729  fzsubel  11730  modadd1  12015  modmul1  12022  seqcaopr  12126  expsub  12195  sqlecan  12256  facndiv  12348  hashss  12456  hashfacen  12485  hashf1lem1  12486  brfi1uzind  12514  swrdccatin12lem2b  12693  2cshwcshw  12775  resqrex  13066  fprodeq0  13761  hashdvds  14287  eulerthlem2  14294  pceu  14352  pcqcl  14362  infpnlem1  14410  4sqlem11  14455  ramcl  14529  imasvscafn  14916  invfun  15140  catcisolem  15412  prfcl  15451  prf1st  15452  prf2nd  15453  1st2ndprf  15454  curfuncf  15486  ipodrsfi  15772  mhmpropd  15951  subsubm  15967  pwsdiagmhm  15979  gsumccat  15988  frmdgsum  16009  grplcan  16081  grplmulf1o  16091  mulgsubcl  16135  subsubg  16203  eqger  16230  resghm  16262  conjghm  16276  orbsta  16330  psgnunilem2  16499  odmulg  16557  sylow2a  16618  sylow3lem1  16626  lsmssv  16642  pj1ghm  16700  frgpup1  16772  ghmplusg  16831  subsubrg  17434  issrngd  17489  lmhmco  17668  lmhmf1o  17671  lmhmima  17672  lmhmpreima  17673  reslmhm  17677  pwsdiaglmhm  17682  pwssplit2  17685  pwssplit3  17686  pj1lmhm  17725  lspdisj  17750  issubassa2  17973  psrbagconf1o  18005  evlslem2  18159  evlslem1  18163  ply1sclf1  18309  prmirred  18503  prmirredOLD  18506  cygznlem3  18586  frlmsslsp  18807  frlmsslspOLD  18808  frlmlbs  18809  frlmup1  18810  mamuass  18882  dmatmul  18977  dmatsubcl  18978  dmatmulcl  18980  dmatcrng  18982  scmatcrng  19001  mdetunilem9  19100  pm2mpghm  19295  fvmptnn04ifb  19330  istps2OLD  19400  toponmre  19572  neiptopreu  19612  ordtbas  19671  txcls  20083  txlm  20127  qtoptop2  20178  qtoprest  20196  kqt0lem  20215  ptuncnv  20286  fmfnfmlem4  20436  alexsubALTlem2  20526  tgpmulg  20570  blin  20902  xmeter  20914  xmetresbl  20918  dscmet  21071  nmdvr  21157  metnrmlem3  21343  icccvx  21428  bndth  21436  htpycc  21458  pcohtpylem  21497  pi1blem  21517  lmmbrf  21679  iscfil2  21683  iscau4  21696  minveclem7  21828  elovolm  21864  dyaddisjlem  21982  ismbfd  22025  itg1mulc  22089  dvlip  22372  dvcvx  22399  plypf1  22587  eff1olem  22913  logccv  23022  lawcos  23126  sqff1o  23434  dvdsppwf1o  23440  dvdsflf1o  23441  fsumdvdsmul  23449  sgmmul  23454  fsumvma  23466  bposlem6  23542  lgsdchr  23601  rpvmasum2  23675  pntpbnd1  23749  ostthlem1  23790  tgbtwntriv2  23856  ercgrg  23886  colinearalglem4  24190  axlowdimlem15  24237  axcontlem7  24251  axcontlem8  24252  axcontlem10  24254  spthonepeq  24567  usgra2adedgspth  24591  usgra2adedgwlk  24592  usgra2adedgwlkon  24593  numclwlk1lem2f1  25072  grpolcan  25213  isgrp2d  25215  nvmf  25519  nvsubadd  25528  sspmval  25624  sspival  25629  nmosetre  25657  sspph  25748  minvecolem7  25777  hiassdi  25986  shscli  26213  fh1  26514  fh2  26515  cm2j  26516  chscllem2  26534  spansncvi  26548  5oalem2  26551  adjsym  26730  nmopsetretALT  26760  nmfnsetre  26774  cnvadj  26789  cnvunop  26815  unoplin  26817  hmoplin  26839  lnopmi  26897  hmops  26917  hmopm  26918  nmcexi  26923  adjlnop  26983  adjmul  26989  adjadd  26990  opsqrlem1  27037  mdsl0  27207  ssmd2  27209  mdexchi  27232  superpos  27251  chrelat2i  27262  atcvatlem  27282  atcvati  27283  chirredlem1  27287  chirredi  27291  atcvat3i  27293  atcvat4i  27294  mdsymlem3  27302  mdsymlem5  27304  cdj3lem2b  27334  isoun  27498  xrge0infss  27558  ddemeas  28186  subfacp1lem3  28604  subfacp1lem5  28606  ghomf1olem  29012  wfi  29263  frind  29299  wfrlem9  29327  sltres  29400  nodenselem6  29422  nodenselem7  29423  nodense  29425  nofulllem5  29442  btwnconn1lem12  29724  colinbtwnle  29744  broutsideof2  29748  lineelsb2  29774  onsuct0  29882  supadd  30018  heicant  30025  mblfinlem2  30028  mblfinlem3  30029  ismblfin  30031  ftc1anclem5  30070  ftc1anclem6  30071  ftc1anc  30074  nn0prpwlem  30116  neibastop2lem  30154  tailfb  30171  sdclem1  30212  seqpo  30216  sstotbnd  30247  cntotbnd  30268  ismtycnv  30274  ismtyres  30280  heibor  30293  exidreslem  30315  ghomdiv  30322  grpokerinj  30323  rngohomco  30353  rngoisoco  30361  idlsubcl  30396  divrngidl  30401  ispridl2  30411  ispridlc  30443  fphpdo  30727  pell1234qrne0  30765  pell14qrgt0  30771  pell1qrge1  30782  monotoddzzfi  30854  expmordi  30859  jm2.18  30906  wepwsolem  30963  dnnumch3  30969  dnwech  30970  kelac1  30985  kercvrlsm  31005  lcmdvds  31190  cncmpmax  31361  mullimc  31576  mullimcf  31583  idlimc  31586  limclner  31611  fperdvper  31669  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  dvnprodlem1  31697  stoweidlem27  31763  stoweidlem48  31784  fourierdlem42  31885  fourierdlem63  31906  fourierdlem65  31908  usgra2adedglem1  32310  mgmhmpropd  32427  subsubmgm  32439  funcestrcsetclem8  32619  fullestrcsetc  32623  embedsetcestrclem  32629  funcsetcestrclem8  32634  fullsetcestrc  32638  srhmsubc  32752  srhmsubcOLD  32771  bnj1145  33917  riotasv3d  34566  omllaw3  34845  omlfh1N  34858  hlrelat2  35002  cvratlem  35020  cvrat  35021  cvrat3  35041  cvrat4  35042  ps-2  35077  elpaddn0  35399  paddss12  35418  pmodlem2  35446  cdleme0cq  35815  cdlemeg49lebilem  36140  cdleme50eq  36142  tendoeq2  36375  tendoex  36576  diameetN  36658  diainN  36659  dvhopN  36718  djajN  36739  dihmeetcl  36947  mapdheq2  37331
  Copyright terms: Public domain W3C validator