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  950  3ad2antr2  1154  3ad2antr3  1155  ordelord  4736  foco  5625  isocnv  6016  isores2  6019  f1oiso2  6038  offval  6322  ordsucun  6431  opabex2  6511  xp2nd  6602  1stconst  6656  2ndconst  6657  smoord  6818  tfrlem9  6836  tfrlem11  6839  oaass  6992  omordi  6997  omwordri  7003  odi  7010  oewordri  7023  nnawordi  7052  nnmordi  7062  dom2lem  7341  fundmen  7375  sbthlem9  7421  mapen  7467  mapunen  7472  ssenen  7477  domfi  7526  mapfien  7649  inf3lem6  7831  mapfienOLD  7919  r1val1  7985  rankval3b  8025  numacn  8211  infxpabs  8373  infxp  8376  cfsmolem  8431  infpssrlem4  8467  fin23lem27  8489  isf34lem4  8538  hsmexlem2  8588  axdc3lem2  8612  axdc3lem4  8614  iundom2g  8696  gchen1  8784  fpwwe2lem7  8795  fpwwe2lem11  8799  fpwwe2lem12  8800  prlem936  9208  muladd  9769  leord1  9859  eqord1  9860  ltord2  9861  leord2  9862  eqord2  9863  divadddiv  10038  ltmul12a  10177  lemul12b  10178  supmullem1  10288  cju  10310  zextlt  10708  zmax  10942  xrre  11133  supxr  11267  ixxdisj  11307  iooshf  11366  icodisj  11402  ioojoin  11408  iccshftr  11411  iccshftl  11413  iccdil  11415  icccntr  11417  iccf1o  11421  fzaddel  11485  fzsubel  11486  modadd1  11737  modmul1  11744  seqcaopr  11835  expsub  11903  sqlecan  11964  facndiv  12056  hashss  12158  hashfacen  12199  hashf1lem1  12200  brfi1uzind  12211  swrdccatin12lem2b  12369  resqrex  12732  hashdvds  13842  eulerthlem2  13849  pceu  13905  pcqcl  13915  infpnlem1  13963  4sqlem11  14008  ramcl  14082  imasvscafn  14467  invfun  14694  catcisolem  14966  prfcl  15005  prf1st  15006  prf2nd  15007  1st2ndprf  15008  curfuncf  15040  ipodrsfi  15325  mhmpropd  15462  subsubm  15476  pwsdiagmhm  15488  gsumccat  15510  frmdgsum  15531  grplcan  15581  grplmulf1o  15591  mulgsubcl  15632  subsubg  15695  eqger  15722  resghm  15754  conjghm  15768  orbsta  15822  psgnunilem2  15992  odmulg  16048  sylow2a  16109  sylow3lem1  16117  lsmssv  16133  pj1ghm  16191  frgpup1  16263  ghmplusg  16319  subsubrg  16869  issrngd  16924  lmhmco  17101  lmhmf1o  17104  lmhmima  17105  lmhmpreima  17106  reslmhm  17110  pwsdiaglmhm  17115  pwssplit2  17118  pwssplit3  17119  pj1lmhm  17158  lspdisj  17183  issubassa2  17392  psrbagconf1o  17421  evlslem2  17572  evlslem1  17576  ply1sclf1  17716  prmirred  17894  prmirredOLD  17897  cygznlem3  17977  frlmsslsp  18198  frlmsslspOLD  18199  frlmlbs  18200  frlmup1  18201  mamuass  18281  mdetunilem9  18401  istps2OLD  18501  toponmre  18672  neiptopreu  18712  ordtbas  18771  txcls  19152  txlm  19196  qtoptop2  19247  qtoprest  19265  kqt0lem  19284  ptuncnv  19355  fmfnfmlem4  19505  alexsubALTlem2  19595  tgpmulg  19639  blin  19971  xmeter  19983  xmetresbl  19987  dscmet  20140  nmdvr  20226  metnrmlem3  20412  icccvx  20497  bndth  20505  htpycc  20527  pcohtpylem  20566  pi1blem  20586  lmmbrf  20748  iscfil2  20752  iscau4  20765  minveclem7  20897  elovolm  20933  dyaddisjlem  21050  ismbfd  21093  itg1mulc  21157  dvlip  21440  dvcvx  21467  plypf1  21655  eff1olem  21979  logccv  22083  lawcos  22187  sqff1o  22495  dvdsppwf1o  22501  dvdsflf1o  22502  fsumdvdsmul  22510  sgmmul  22515  fsumvma  22527  bposlem6  22603  lgsdchr  22662  rpvmasum2  22736  pntpbnd1  22810  ostthlem1  22851  tgbtwntriv2  22916  ercgrg  22944  colinearalglem4  23106  axlowdimlem15  23153  axcontlem7  23167  axcontlem8  23168  axcontlem10  23170  spthonepeq  23437  grpolcan  23671  isgrp2d  23673  nvmf  23977  nvsubadd  23986  sspmval  24082  sspival  24087  nmosetre  24115  sspph  24206  minvecolem7  24235  hiassdi  24444  shscli  24671  fh1  24972  fh2  24973  cm2j  24974  chscllem2  24992  spansncvi  25006  5oalem2  25009  adjsym  25188  nmopsetretALT  25218  nmfnsetre  25232  cnvadj  25247  cnvunop  25273  unoplin  25275  hmoplin  25297  lnopmi  25355  hmops  25375  hmopm  25376  nmcexi  25381  adjlnop  25441  adjmul  25447  adjadd  25448  opsqrlem1  25495  mdsl0  25665  ssmd2  25667  mdexchi  25690  superpos  25709  chrelat2i  25720  atcvatlem  25740  atcvati  25741  chirredlem1  25745  chirredi  25749  atcvat3i  25751  atcvat4i  25752  mdsymlem3  25760  mdsymlem5  25762  cdj3lem2b  25792  isoun  25948  xrge0infss  26004  ddemeas  26604  afsval  26947  subfacp1lem3  27022  subfacp1lem5  27024  ghomf1olem  27264  fprodeq0  27437  wfi  27619  frind  27655  wfrlem9  27683  sltres  27756  nodenselem6  27778  nodenselem7  27779  nodense  27781  nofulllem5  27798  btwnconn1lem12  28080  colinbtwnle  28100  broutsideof2  28104  lineelsb2  28130  onsuct0  28239  supadd  28371  heicant  28379  mblfinlem2  28382  mblfinlem3  28383  ismblfin  28385  ftc1anclem5  28424  ftc1anclem6  28425  ftc1anc  28428  nn0prpwlem  28470  neibastop2lem  28534  tailfb  28551  sdclem1  28592  seqpo  28596  sstotbnd  28627  cntotbnd  28648  ismtycnv  28654  ismtyres  28660  heibor  28673  exidreslem  28695  ghomdiv  28702  grpokerinj  28703  rngohomco  28733  rngoisoco  28741  idlsubcl  28776  divrngidl  28781  ispridl2  28791  ispridlc  28823  fphpdo  29109  pell1234qrne0  29147  pell14qrgt0  29153  pell1qrge1  29164  monotoddzzfi  29236  expmordi  29241  jm2.18  29290  wepwsolem  29347  dnnumch3  29353  dnwech  29354  kelac1  29369  kercvrlsm  29389  cncmpmax  29707  stoweidlem27  29775  stoweidlem48  29796  usgra2adedgspth  30258  usgra2adedgwlk  30259  usgra2adedgwlkon  30260  usgra2adedglem1  30261  cshwlemma1  30442  numclwlk1lem2f1  30640  dmatmul  30799  bnj1145  31871  riotasv3d  32451  omllaw3  32730  omlfh1N  32743  hlrelat2  32887  cvratlem  32905  cvrat  32906  cvrat3  32926  cvrat4  32927  ps-2  32962  elpaddn0  33284  paddss12  33303  pmodlem2  33331  cdleme0cq  33699  cdlemeg49lebilem  34023  cdleme50eq  34025  tendoeq2  34258  tendoex  34459  diameetN  34541  diainN  34542  dvhopN  34601  djajN  34622  dihmeetcl  34830  mapdheq2  35214
  Copyright terms: Public domain W3C validator