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

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

Proof of Theorem adantrl
StepHypRef Expression
1 simpr 448 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan2 461 1  |-  ( (
ph  /\  ( th  /\  ps ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  ad2ant2l  727  ad2ant2rl  730  consensus  926  3ad2antr2  1123  3ad2antr3  1124  sbcom  2138  ordelord  4563  ordsucun  4764  foco  5622  isocnv  6009  isores2  6012  f1oiso2  6031  offval  6271  xp2nd  6336  1stconst  6394  2ndconst  6395  riotasv3d  6557  riotasv3dOLD  6558  smoord  6586  tfrlem9  6605  tfrlem11  6608  oaass  6763  omordi  6768  omwordri  6774  odi  6781  oewordri  6794  nnawordi  6823  nnmordi  6833  dom2lem  7106  fundmen  7139  sbthlem9  7184  mapen  7230  mapunen  7235  ssenen  7240  domfi  7289  inf3lem6  7544  mapfien  7609  r1val1  7668  rankval3b  7708  numacn  7886  infxpabs  8048  infxp  8051  cfsmolem  8106  infpssrlem4  8142  fin23lem27  8164  isf34lem4  8213  hsmexlem2  8263  axdc3lem2  8287  axdc3lem4  8289  iundom2g  8371  gchen1  8456  fpwwe2lem7  8467  fpwwe2lem11  8471  fpwwe2lem12  8472  prlem936  8880  muladd  9422  leord1  9510  eqord1  9511  ltord2  9512  leord2  9513  eqord2  9514  divadddiv  9685  ltmul12a  9822  lemul12b  9823  supmullem1  9930  cju  9952  zextlt  10300  zmax  10527  xrre  10713  supxr  10847  ixxdisj  10887  iooshf  10945  icodisj  10978  ioojoin  10983  iccshftr  10986  iccshftl  10988  iccdil  10990  icccntr  10992  iccf1o  10995  fzaddel  11043  fzsubel  11044  modadd1  11233  modmul1  11234  seqcaopr  11315  expsub  11382  sqlecan  11442  facndiv  11534  hashfacen  11658  hashf1lem1  11659  brfi1uzind  11670  resqrex  12011  hashdvds  13119  eulerthlem2  13126  pceu  13175  pcqcl  13185  infpnlem1  13233  4sqlem11  13278  ramcl  13352  imasvscafn  13717  invfun  13944  catcisolem  14216  prfcl  14255  prf1st  14256  prf2nd  14257  1st2ndprf  14258  curfuncf  14290  ipodrsfi  14544  mhmpropd  14699  subsubm  14712  pwsdiagmhm  14723  gsumccat  14742  frmdgsum  14762  grplcan  14812  grplmulf1o  14820  mulgsubcl  14859  subsubg  14918  eqger  14945  resghm  14977  conjghm  14991  orbsta  15045  odmulg  15147  sylow2a  15208  sylow3lem1  15216  lsmssv  15232  pj1ghm  15290  frgpup1  15362  ghmplusg  15416  subsubrg  15849  issrngd  15904  lmhmco  16074  lmhmf1o  16077  lmhmima  16078  lmhmpreima  16079  reslmhm  16083  pwsdiaglmhm  16088  pj1lmhm  16127  lspdisj  16152  issubassa2  16358  psrbagconf1o  16394  evlslem2  16523  ply1sclf1  16635  prmirred  16730  cygznlem3  16805  istps2OLD  16941  toponmre  17112  neiptopreu  17152  ordtbas  17210  txcls  17589  txlm  17633  qtoptop2  17684  qtoprest  17702  kqt0lem  17721  ptuncnv  17792  fmfnfmlem4  17942  alexsubALTlem2  18032  tgpmulg  18076  blin  18404  xmeter  18416  xmetresbl  18420  dscmet  18573  nmdvr  18659  metnrmlem3  18844  icccvx  18928  bndth  18936  htpycc  18958  pcohtpylem  18997  pi1blem  19017  lmmbrf  19168  iscfil2  19172  iscau4  19185  minveclem7  19289  elovolm  19324  dyaddisjlem  19440  ismbfd  19485  itg1mulc  19549  dvlip  19830  dvcvx  19857  evlslem1  19889  plypf1  20084  eff1olem  20403  logccv  20507  lawcos  20611  sqff1o  20918  dvdsppwf1o  20924  dvdsflf1o  20925  fsumdvdsmul  20933  sgmmul  20938  fsumvma  20950  bposlem6  21026  lgsdchr  21085  rpvmasum2  21159  pntpbnd1  21233  ostthlem1  21274  spthonepeq  21540  grpolcan  21774  isgrp2d  21776  nvmf  22080  nvsubadd  22089  sspmval  22185  sspival  22190  nmosetre  22218  sspph  22309  minvecolem7  22338  hiassdi  22546  shscli  22772  fh1  23073  fh2  23074  cm2j  23075  chscllem2  23093  spansncvi  23107  5oalem2  23110  adjsym  23289  nmopsetretALT  23319  nmfnsetre  23333  cnvadj  23348  cnvunop  23374  unoplin  23376  hmoplin  23398  lnopmi  23456  hmops  23476  hmopm  23477  nmcexi  23482  adjlnop  23542  adjmul  23548  adjadd  23549  opsqrlem1  23596  mdsl0  23766  ssmd2  23768  mdexchi  23791  superpos  23810  chrelat2i  23821  atcvatlem  23841  atcvati  23842  chirredlem1  23846  chirredi  23850  atcvat3i  23852  atcvat4i  23853  mdsymlem3  23861  mdsymlem5  23863  cdj3lem2b  23893  isoun  24042  subfacp1lem3  24821  subfacp1lem5  24823  ghomf1olem  25058  fprodeq0  25252  wfi  25421  frind  25457  wfrlem9  25478  sltres  25532  nodenselem6  25554  nodenselem7  25555  nodense  25557  nofulllem5  25574  colinearalglem4  25752  axlowdimlem15  25799  axcontlem7  25813  axcontlem8  25814  axcontlem10  25816  btwnconn1lem12  25936  colinbtwnle  25956  broutsideof2  25960  lineelsb2  25986  onsuct0  26095  supadd  26138  mblfinlem  26143  mblfinlem2  26144  ismblfin  26146  nn0prpwlem  26215  neibastop2lem  26279  tailfb  26296  sdclem1  26337  seqpo  26341  sstotbnd  26374  cntotbnd  26395  ismtycnv  26401  ismtyres  26407  heibor  26420  exidreslem  26442  ghomdiv  26449  grpokerinj  26450  rngohomco  26480  rngoisoco  26488  idlsubcl  26523  divrngidl  26528  ispridl2  26538  ispridlc  26570  fphpdo  26768  pell1234qrne0  26806  pell14qrgt0  26812  pell1qrge1  26823  monotoddzzfi  26895  expmordi  26900  jm2.18  26949  wepwsolem  27006  dnnumch3  27012  dnwech  27013  kelac1  27029  kercvrlsm  27049  pwssplit2  27057  pwssplit3  27058  frlmsslsp  27116  frlmlbs  27117  frlmup1  27118  psgnunilem2  27286  mamuass  27328  cncmpmax  27570  stoweidlem27  27643  stoweidlem48  27664  swrdccatin2  28018  swrdccatin12  28026  usgra2adedgspth  28045  usgra2adedgwlk  28046  usgra2adedgwlkon  28047  usgra2adedglem1  28048  bnj1145  29068  sbcomwAUX7  29291  sbcomOLD7  29439  omllaw3  29728  omlfh1N  29741  hlrelat2  29885  cvratlem  29903  cvrat  29904  cvrat3  29924  cvrat4  29925  ps-2  29960  elpaddn0  30282  paddss12  30301  pmodlem2  30329  cdleme0cq  30697  cdlemeg49lebilem  31021  cdleme50eq  31023  tendoeq2  31256  tendoex  31457  diameetN  31539  diainN  31540  dvhopN  31599  djajN  31620  dihmeetcl  31828  mapdheq2  32212
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