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

Theorem adantrl 696
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 447 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan2 460 1  |-  ( (
ph  /\  ( th  /\  ps ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  ad2ant2l  726  ad2ant2rl  729  consensus  925  3ad2antr2  1121  3ad2antr3  1122  sbcom  2029  ordelord  4414  ordsucun  4616  foco  5461  isocnv  5827  isores2  5830  f1oiso2  5849  offval  6085  xp2nd  6150  1stconst  6207  2ndconst  6208  riotasv3d  6353  riotasv3dOLD  6354  smoord  6382  tfrlem9  6401  tfrlem11  6404  oaass  6559  omordi  6564  omwordri  6570  odi  6577  oewordri  6590  nnawordi  6619  nnmordi  6629  dom2lem  6901  fundmen  6934  sbthlem9  6979  mapen  7025  mapunen  7030  ssenen  7035  domfi  7084  inf3lem6  7334  mapfien  7399  r1val1  7458  rankval3b  7498  numacn  7676  infxpabs  7838  infxp  7841  cfsmolem  7896  infpssrlem4  7932  fin23lem27  7954  isf34lem4  8003  hsmexlem2  8053  axdc3lem2  8077  axdc3lem4  8079  iundom2g  8162  gchen1  8247  fpwwe2lem7  8258  fpwwe2lem11  8262  fpwwe2lem12  8263  prlem936  8671  muladd  9212  leord1  9300  eqord1  9301  ltord2  9302  leord2  9303  eqord2  9304  divadddiv  9475  ltmul12a  9612  lemul12b  9613  supmullem1  9720  cju  9742  zextlt  10086  zmax  10313  xrre  10498  supxr  10631  ixxdisj  10671  iooshf  10728  icodisj  10761  ioojoin  10766  iccshftr  10769  iccshftl  10771  iccdil  10773  icccntr  10775  iccf1o  10778  fzaddel  10826  fzsubel  10827  modadd1  11001  modmul1  11002  seqcaopr  11083  expsub  11149  sqlecan  11209  facndiv  11301  hashfacen  11392  hashf1lem1  11393  resqrex  11736  hashdvds  12843  eulerthlem2  12850  pceu  12899  pcqcl  12909  infpnlem1  12957  4sqlem11  13002  ramcl2lem  13056  ramcl  13076  imasvscafn  13439  invfun  13666  catcisolem  13938  prfcl  13977  prf1st  13978  prf2nd  13979  1st2ndprf  13980  curfuncf  14012  ipodrsfi  14266  mhmpropd  14421  subsubm  14434  pwsdiagmhm  14445  gsumccat  14464  frmdgsum  14484  grplcan  14534  grplmulf1o  14542  mulgsubcl  14581  subsubg  14640  eqger  14667  resghm  14699  conjghm  14713  orbsta  14767  odmulg  14869  sylow2a  14930  sylow3lem1  14938  lsmssv  14954  pj1ghm  15012  frgpup1  15084  ghmplusg  15138  subsubrg  15571  issrngd  15626  lmhmco  15800  lmhmf1o  15803  lmhmima  15804  lmhmpreima  15805  reslmhm  15809  pwsdiaglmhm  15814  pj1lmhm  15853  lspdisj  15878  issubassa2  16084  psrbagconf1o  16120  evlslem2  16249  ply1sclf1  16364  prmirred  16448  cygznlem3  16523  istps2OLD  16659  toponmre  16830  ordtbas  16922  txcls  17299  txlm  17342  qtoptop2  17390  qtoprest  17408  kqt0lem  17427  ptuncnv  17498  fmfnfmlem4  17652  alexsubALTlem2  17742  tgpmulg  17776  blin  17970  xmeter  17979  xmetresbl  17983  dscmet  18095  nmdvr  18181  metnrmlem3  18365  icccvx  18448  bndth  18456  htpycc  18478  pcohtpylem  18517  pi1blem  18537  lmmbrf  18688  iscfil2  18692  iscau4  18705  minveclem7  18799  elovolm  18834  dyaddisjlem  18950  ismbfd  18995  itg1mulc  19059  dvlip  19340  dvcvx  19367  evlslem1  19399  plypf1  19594  eff1olem  19910  logccv  20010  lawcos  20114  sqff1o  20420  dvdsppwf1o  20426  dvdsflf1o  20427  fsumdvdsmul  20435  sgmmul  20440  fsumvma  20452  bposlem6  20528  lgsdchr  20587  rpvmasum2  20661  pntpbnd1  20735  ostthlem1  20776  grpolcan  20900  isgrp2d  20902  nvmf  21204  nvsubadd  21213  sspmval  21309  sspival  21314  nmosetre  21342  sspph  21433  minvecolem7  21462  hiassdi  21670  shscli  21896  fh1  22197  fh2  22198  cm2j  22199  chscllem2  22217  spansncvi  22231  5oalem2  22234  adjsym  22413  nmopsetretALT  22443  nmfnsetre  22457  cnvadj  22472  cnvunop  22498  unoplin  22500  hmoplin  22522  lnopmi  22580  hmops  22600  hmopm  22601  nmcexi  22606  adjlnop  22666  adjmul  22672  adjadd  22673  opsqrlem1  22720  mdsl0  22890  ssmd2  22892  mdexchi  22915  superpos  22934  chrelat2i  22945  atcvatlem  22965  atcvati  22966  chirredlem1  22970  chirredi  22974  atcvat3i  22976  atcvat4i  22977  mdsymlem3  22985  mdsymlem5  22987  cdj3lem2b  23017  subfacp1lem3  23124  subfacp1lem5  23126  ghomf1olem  23412  wfi  23618  frind  23654  wfrlem9  23675  sltres  23729  nodenselem6  23751  nodenselem7  23752  nodense  23754  nofulllem5  23771  colinearalglem4  23948  axlowdimlem15  23995  axcontlem7  24009  axcontlem8  24010  axcontlem10  24012  btwnconn1lem12  24132  colinbtwnle  24152  broutsideof2  24156  lineelsb2  24182  onsuct0  24291  preotr2  24647  fprodadd  24764  mvecrtol  24885  cmp2morp  25370  rocatval  25371  nn0prpwlem  25650  neibastop2lem  25721  tailfb  25738  sdclem1  25865  seqpo  25869  sstotbnd  25911  cntotbnd  25932  ismtycnv  25938  ismtyres  25944  heibor  25957  exidreslem  25979  ghomdiv  25986  grpokerinj  25987  rngohomco  26017  rngoisoco  26025  idlsubcl  26060  divrngidl  26065  ispridl2  26075  ispridlc  26107  fphpdo  26312  pell1234qrne0  26350  pell14qrgt0  26356  pell1qrge1  26367  monotoddzzfi  26439  expmordi  26444  jm2.18  26493  wepwsolem  26550  dnnumch3  26556  dnwech  26557  kelac1  26573  kercvrlsm  26593  pwssplit2  26601  pwssplit3  26602  frlmsslsp  26660  frlmlbs  26661  frlmup1  26662  psgnunilem2  26830  mamuass  26872  stoweidlem48  27209  bnj1145  28396  omllaw3  28808  omlfh1N  28821  hlrelat2  28965  cvratlem  28983  cvrat  28984  cvrat3  29004  cvrat4  29005  ps-2  29040  elpaddn0  29362  paddss12  29381  pmodlem2  29409  cdleme0cq  29777  cdlemeg49lebilem  30101  cdleme50eq  30103  tendoeq2  30336  tendoex  30537  diameetN  30619  diainN  30620  dvhopN  30679  djajN  30700  dihmeetcl  30908  mapdheq2  31292
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