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

Theorem adantrl 708
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 458 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan2 471 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  738  ad2ant2rl  741  consensus  943  3ad2antr2  1147  3ad2antr3  1148  sbcomOLD  2118  ordelord  4728  foco  5618  isocnv  6008  isores2  6011  f1oiso2  6030  offval  6316  ordsucun  6425  opabex2  6505  xp2nd  6596  1stconst  6650  2ndconst  6651  smoord  6812  tfrlem9  6830  tfrlem11  6833  oaass  6988  omordi  6993  omwordri  6999  odi  7006  oewordri  7019  nnawordi  7048  nnmordi  7058  dom2lem  7337  fundmen  7371  sbthlem9  7417  mapen  7463  mapunen  7468  ssenen  7473  domfi  7522  mapfien  7645  inf3lem6  7827  mapfienOLD  7915  r1val1  7981  rankval3b  8021  numacn  8207  infxpabs  8369  infxp  8372  cfsmolem  8427  infpssrlem4  8463  fin23lem27  8485  isf34lem4  8534  hsmexlem2  8584  axdc3lem2  8608  axdc3lem4  8610  iundom2g  8692  gchen1  8780  fpwwe2lem7  8791  fpwwe2lem11  8795  fpwwe2lem12  8796  prlem936  9204  muladd  9765  leord1  9855  eqord1  9856  ltord2  9857  leord2  9858  eqord2  9859  divadddiv  10034  ltmul12a  10173  lemul12b  10174  supmullem1  10284  cju  10306  zextlt  10704  zmax  10938  xrre  11129  supxr  11263  ixxdisj  11303  iooshf  11362  icodisj  11397  ioojoin  11403  iccshftr  11406  iccshftl  11408  iccdil  11410  icccntr  11412  iccf1o  11416  fzaddel  11480  fzsubel  11481  modadd1  11729  modmul1  11736  seqcaopr  11827  expsub  11895  sqlecan  11956  facndiv  12048  hashss  12150  hashfacen  12191  hashf1lem1  12192  brfi1uzind  12203  swrdccatin12lem2b  12361  resqrex  12724  hashdvds  13833  eulerthlem2  13840  pceu  13896  pcqcl  13906  infpnlem1  13954  4sqlem11  13999  ramcl  14073  imasvscafn  14458  invfun  14685  catcisolem  14957  prfcl  14996  prf1st  14997  prf2nd  14998  1st2ndprf  14999  curfuncf  15031  ipodrsfi  15316  mhmpropd  15453  subsubm  15467  pwsdiagmhm  15479  gsumccat  15499  frmdgsum  15520  grplcan  15570  grplmulf1o  15580  mulgsubcl  15621  subsubg  15684  eqger  15711  resghm  15743  conjghm  15757  orbsta  15811  psgnunilem2  15981  odmulg  16037  sylow2a  16098  sylow3lem1  16106  lsmssv  16122  pj1ghm  16180  frgpup1  16252  ghmplusg  16308  subsubrg  16815  issrngd  16870  lmhmco  17046  lmhmf1o  17049  lmhmima  17050  lmhmpreima  17051  reslmhm  17055  pwsdiaglmhm  17060  pwssplit2  17063  pwssplit3  17064  pj1lmhm  17103  lspdisj  17128  issubassa2  17337  psrbagconf1o  17378  evlslem2  17525  ply1sclf1  17639  prmirred  17761  prmirredOLD  17764  cygznlem3  17844  frlmsslsp  18065  frlmsslspOLD  18066  frlmlbs  18067  frlmup1  18068  mamuass  18148  mdetunilem9  18268  istps2OLD  18368  toponmre  18539  neiptopreu  18579  ordtbas  18638  txcls  19019  txlm  19063  qtoptop2  19114  qtoprest  19132  kqt0lem  19151  ptuncnv  19222  fmfnfmlem4  19372  alexsubALTlem2  19462  tgpmulg  19506  blin  19838  xmeter  19850  xmetresbl  19854  dscmet  20007  nmdvr  20093  metnrmlem3  20279  icccvx  20364  bndth  20372  htpycc  20394  pcohtpylem  20433  pi1blem  20453  lmmbrf  20615  iscfil2  20619  iscau4  20632  minveclem7  20764  elovolm  20800  dyaddisjlem  20917  ismbfd  20960  itg1mulc  21024  dvlip  21307  dvcvx  21334  evlslem1  21367  plypf1  21565  eff1olem  21889  logccv  21993  lawcos  22097  sqff1o  22405  dvdsppwf1o  22411  dvdsflf1o  22412  fsumdvdsmul  22420  sgmmul  22425  fsumvma  22437  bposlem6  22513  lgsdchr  22572  rpvmasum2  22646  pntpbnd1  22720  ostthlem1  22761  tgbtwntriv2  22823  ercgrg  22850  colinearalglem4  22978  axlowdimlem15  23025  axcontlem7  23039  axcontlem8  23040  axcontlem10  23042  spthonepeq  23309  grpolcan  23543  isgrp2d  23545  nvmf  23849  nvsubadd  23858  sspmval  23954  sspival  23959  nmosetre  23987  sspph  24078  minvecolem7  24107  hiassdi  24316  shscli  24543  fh1  24844  fh2  24845  cm2j  24846  chscllem2  24864  spansncvi  24878  5oalem2  24881  adjsym  25060  nmopsetretALT  25090  nmfnsetre  25104  cnvadj  25119  cnvunop  25145  unoplin  25147  hmoplin  25169  lnopmi  25227  hmops  25247  hmopm  25248  nmcexi  25253  adjlnop  25313  adjmul  25319  adjadd  25320  opsqrlem1  25367  mdsl0  25537  ssmd2  25539  mdexchi  25562  superpos  25581  chrelat2i  25592  atcvatlem  25612  atcvati  25613  chirredlem1  25617  chirredi  25621  atcvat3i  25623  atcvat4i  25624  mdsymlem3  25632  mdsymlem5  25634  cdj3lem2b  25664  isoun  25821  ddemeas  26506  afsval  26843  subfacp1lem3  26918  subfacp1lem5  26920  ghomf1olem  27160  fprodeq0  27333  wfi  27515  frind  27551  wfrlem9  27579  sltres  27652  nodenselem6  27674  nodenselem7  27675  nodense  27677  nofulllem5  27694  btwnconn1lem12  27976  colinbtwnle  27996  broutsideof2  28000  lineelsb2  28026  onsuct0  28135  supadd  28262  heicant  28270  mblfinlem2  28273  mblfinlem3  28274  ismblfin  28276  ftc1anclem5  28315  ftc1anclem6  28316  ftc1anc  28319  nn0prpwlem  28361  neibastop2lem  28425  tailfb  28442  sdclem1  28483  seqpo  28487  sstotbnd  28518  cntotbnd  28539  ismtycnv  28545  ismtyres  28551  heibor  28564  exidreslem  28586  ghomdiv  28593  grpokerinj  28594  rngohomco  28624  rngoisoco  28632  idlsubcl  28667  divrngidl  28672  ispridl2  28682  ispridlc  28714  fphpdo  29001  pell1234qrne0  29039  pell14qrgt0  29045  pell1qrge1  29056  monotoddzzfi  29128  expmordi  29133  jm2.18  29182  wepwsolem  29239  dnnumch3  29245  dnwech  29246  kelac1  29261  kercvrlsm  29281  cncmpmax  29599  stoweidlem27  29668  stoweidlem48  29689  usgra2adedgspth  30151  usgra2adedgwlk  30152  usgra2adedgwlkon  30153  usgra2adedglem1  30154  cshwlemma1  30335  numclwlk1lem2f1  30533  bnj1145  31686  riotasv3d  32184  omllaw3  32463  omlfh1N  32476  hlrelat2  32620  cvratlem  32638  cvrat  32639  cvrat3  32659  cvrat4  32660  ps-2  32695  elpaddn0  33017  paddss12  33036  pmodlem2  33064  cdleme0cq  33432  cdlemeg49lebilem  33756  cdleme50eq  33758  tendoeq2  33991  tendoex  34192  diameetN  34274  diainN  34275  dvhopN  34334  djajN  34355  dihmeetcl  34563  mapdheq2  34947
  Copyright terms: Public domain W3C validator