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  2042  ordelord  4430  ordsucun  4632  foco  5477  isocnv  5843  isores2  5846  f1oiso2  5865  offval  6101  xp2nd  6166  1stconst  6223  2ndconst  6224  riotasv3d  6369  riotasv3dOLD  6370  smoord  6398  tfrlem9  6417  tfrlem11  6420  oaass  6575  omordi  6580  omwordri  6586  odi  6593  oewordri  6606  nnawordi  6635  nnmordi  6645  dom2lem  6917  fundmen  6950  sbthlem9  6995  mapen  7041  mapunen  7046  ssenen  7051  domfi  7100  inf3lem6  7350  mapfien  7415  r1val1  7474  rankval3b  7514  numacn  7692  infxpabs  7854  infxp  7857  cfsmolem  7912  infpssrlem4  7948  fin23lem27  7970  isf34lem4  8019  hsmexlem2  8069  axdc3lem2  8093  axdc3lem4  8095  iundom2g  8178  gchen1  8263  fpwwe2lem7  8274  fpwwe2lem11  8278  fpwwe2lem12  8279  prlem936  8687  muladd  9228  leord1  9316  eqord1  9317  ltord2  9318  leord2  9319  eqord2  9320  divadddiv  9491  ltmul12a  9628  lemul12b  9629  supmullem1  9736  cju  9758  zextlt  10102  zmax  10329  xrre  10514  supxr  10647  ixxdisj  10687  iooshf  10744  icodisj  10777  ioojoin  10782  iccshftr  10785  iccshftl  10787  iccdil  10789  icccntr  10791  iccf1o  10794  fzaddel  10842  fzsubel  10843  modadd1  11017  modmul1  11018  seqcaopr  11099  expsub  11165  sqlecan  11225  facndiv  11317  hashfacen  11408  hashf1lem1  11409  resqrex  11752  hashdvds  12859  eulerthlem2  12866  pceu  12915  pcqcl  12925  infpnlem1  12973  4sqlem11  13018  ramcl2lem  13072  ramcl  13092  imasvscafn  13455  invfun  13682  catcisolem  13954  prfcl  13993  prf1st  13994  prf2nd  13995  1st2ndprf  13996  curfuncf  14028  ipodrsfi  14282  mhmpropd  14437  subsubm  14450  pwsdiagmhm  14461  gsumccat  14480  frmdgsum  14500  grplcan  14550  grplmulf1o  14558  mulgsubcl  14597  subsubg  14656  eqger  14683  resghm  14715  conjghm  14729  orbsta  14783  odmulg  14885  sylow2a  14946  sylow3lem1  14954  lsmssv  14970  pj1ghm  15028  frgpup1  15100  ghmplusg  15154  subsubrg  15587  issrngd  15642  lmhmco  15816  lmhmf1o  15819  lmhmima  15820  lmhmpreima  15821  reslmhm  15825  pwsdiaglmhm  15830  pj1lmhm  15869  lspdisj  15894  issubassa2  16100  psrbagconf1o  16136  evlslem2  16265  ply1sclf1  16380  prmirred  16464  cygznlem3  16539  istps2OLD  16675  toponmre  16846  ordtbas  16938  txcls  17315  txlm  17358  qtoptop2  17406  qtoprest  17424  kqt0lem  17443  ptuncnv  17514  fmfnfmlem4  17668  alexsubALTlem2  17758  tgpmulg  17792  blin  17986  xmeter  17995  xmetresbl  17999  dscmet  18111  nmdvr  18197  metnrmlem3  18381  icccvx  18464  bndth  18472  htpycc  18494  pcohtpylem  18533  pi1blem  18553  lmmbrf  18704  iscfil2  18708  iscau4  18721  minveclem7  18815  elovolm  18850  dyaddisjlem  18966  ismbfd  19011  itg1mulc  19075  dvlip  19356  dvcvx  19383  evlslem1  19415  plypf1  19610  eff1olem  19926  logccv  20026  lawcos  20130  sqff1o  20436  dvdsppwf1o  20442  dvdsflf1o  20443  fsumdvdsmul  20451  sgmmul  20456  fsumvma  20468  bposlem6  20544  lgsdchr  20603  rpvmasum2  20677  pntpbnd1  20751  ostthlem1  20792  grpolcan  20916  isgrp2d  20918  nvmf  21220  nvsubadd  21229  sspmval  21325  sspival  21330  nmosetre  21358  sspph  21449  minvecolem7  21478  hiassdi  21686  shscli  21912  fh1  22213  fh2  22214  cm2j  22215  chscllem2  22233  spansncvi  22247  5oalem2  22250  adjsym  22429  nmopsetretALT  22459  nmfnsetre  22473  cnvadj  22488  cnvunop  22514  unoplin  22516  hmoplin  22538  lnopmi  22596  hmops  22616  hmopm  22617  nmcexi  22622  adjlnop  22682  adjmul  22688  adjadd  22689  opsqrlem1  22736  mdsl0  22906  ssmd2  22908  mdexchi  22931  superpos  22950  chrelat2i  22961  atcvatlem  22981  atcvati  22982  chirredlem1  22986  chirredi  22990  atcvat3i  22992  atcvat4i  22993  mdsymlem3  23001  mdsymlem5  23003  cdj3lem2b  23033  isoun  23257  subfacp1lem3  23728  subfacp1lem5  23730  ghomf1olem  24016  wfi  24278  frind  24314  wfrlem9  24335  sltres  24389  nodenselem6  24411  nodenselem7  24412  nodense  24414  nofulllem5  24431  colinearalglem4  24609  axlowdimlem15  24656  axcontlem7  24670  axcontlem8  24671  axcontlem10  24673  btwnconn1lem12  24793  colinbtwnle  24813  broutsideof2  24817  lineelsb2  24843  onsuct0  24952  supadd  24996  preotr2  25338  fprodadd  25455  mvecrtol  25576  cmp2morp  26061  rocatval  26062  nn0prpwlem  26341  neibastop2lem  26412  tailfb  26429  sdclem1  26556  seqpo  26560  sstotbnd  26602  cntotbnd  26623  ismtycnv  26629  ismtyres  26635  heibor  26648  exidreslem  26670  ghomdiv  26677  grpokerinj  26678  rngohomco  26708  rngoisoco  26716  idlsubcl  26751  divrngidl  26756  ispridl2  26766  ispridlc  26798  fphpdo  27003  pell1234qrne0  27041  pell14qrgt0  27047  pell1qrge1  27058  monotoddzzfi  27130  expmordi  27135  jm2.18  27184  wepwsolem  27241  dnnumch3  27247  dnwech  27248  kelac1  27264  kercvrlsm  27284  pwssplit2  27292  pwssplit3  27293  frlmsslsp  27351  frlmlbs  27352  frlmup1  27353  psgnunilem2  27521  mamuass  27563  stoweidlem48  27900  bnj1145  29339  sbcomwAUX7  29562  sbcomOLD7  29709  omllaw3  30057  omlfh1N  30070  hlrelat2  30214  cvratlem  30232  cvrat  30233  cvrat3  30253  cvrat4  30254  ps-2  30289  elpaddn0  30611  paddss12  30630  pmodlem2  30658  cdleme0cq  31026  cdlemeg49lebilem  31350  cdleme50eq  31352  tendoeq2  31585  tendoex  31786  diameetN  31868  diainN  31869  dvhopN  31928  djajN  31949  dihmeetcl  32157  mapdheq2  32541
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