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

Theorem adantrl 720
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 462 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan2 476 1  |-  ( (
ph  /\  ( th  /\  ps ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  ad2ant2l  750  ad2ant2rl  753  consensus  967  cases2  980  3ad2antr2  1171  3ad2antr3  1172  wfi  5432  ordelord  5464  foco  5820  isocnv  6236  isores2  6239  f1oiso2  6258  offval  6552  ordsucun  6666  opabex2  6745  xp2nd  6838  1stconst  6895  2ndconst  6896  wfrdmcl  7055  smoord  7095  tfrlem9  7114  tfrlem11  7117  oaass  7273  omordi  7278  omwordri  7284  odi  7291  oewordri  7304  nnawordi  7333  nnmordi  7343  dom2lem  7619  fundmen  7653  sbthlem9  7699  mapen  7745  mapunen  7750  ssenen  7755  domfi  7802  mapfien  7930  inf3lem6  8147  r1val1  8265  rankval3b  8305  numacn  8487  infxpabs  8649  infxp  8652  cfsmolem  8707  infpssrlem4  8743  fin23lem27  8765  isf34lem4  8814  hsmexlem2  8864  axdc3lem2  8888  axdc3lem4  8890  iundom2g  8972  gchen1  9057  fpwwe2lem7  9068  fpwwe2lem11  9072  fpwwe2lem12  9073  prlem936  9479  muladd  10058  leord1  10148  eqord1  10149  ltord2  10150  leord2  10151  eqord2  10152  divadddiv  10329  ltmul12a  10468  lemul12b  10469  supadd  10582  supmullem1  10584  cju  10612  zextlt  11017  zmax  11268  xrre  11471  supxr  11605  ixxdisj  11657  iooshf  11720  icodisj  11764  ioojoin  11770  iccshftr  11773  iccshftl  11775  iccdil  11777  icccntr  11779  iccf1o  11783  fzaddel  11840  fzsubel  11841  modadd1  12140  modmul1  12149  seqcaopr  12256  expsub  12326  sqlecan  12387  facndiv  12479  hashss  12592  hashfacen  12621  hashf1lem1  12622  fi1uzind  12654  brfi1indALT  12657  swrdccatin12lem2b  12844  2cshwcshw  12926  resqrex  13314  fprodeq0  14028  lcmdvds  14572  hashdvds  14722  eulerthlem2  14729  pceu  14795  pcqcl  14805  infpnlem1  14853  4sqlem11  14898  ramcl  14986  prmgaplem5  15024  imasvscafn  15442  invfun  15668  initoeu2lem2  15909  catcisolem  16000  funcestrcsetclem8  16031  fullestrcsetc  16035  embedsetcestrclem  16041  funcsetcestrclem8  16046  fullsetcestrc  16050  prfcl  16087  prf1st  16088  prf2nd  16089  1st2ndprf  16090  curfuncf  16122  ipodrsfi  16408  mhmpropd  16587  subsubm  16603  pwsdiagmhm  16615  gsumccat  16624  frmdgsum  16645  grplcan  16717  grplmulf1o  16727  mulgsubcl  16771  subsubg  16839  eqger  16866  resghm  16898  conjghm  16912  orbsta  16966  psgnunilem2  17135  odmulg  17206  sylow2a  17270  sylow3lem1  17278  lsmssv  17294  pj1ghm  17352  frgpup1  17424  ghmplusg  17483  subsubrg  18033  issrngd  18088  lmhmco  18265  lmhmf1o  18268  lmhmima  18269  lmhmpreima  18270  reslmhm  18274  pwsdiaglmhm  18279  pwssplit2  18282  pwssplit3  18283  pj1lmhm  18322  lspdisj  18347  issubassa2  18568  psrbagconf1o  18597  evlslem2  18734  evlslem1  18737  ply1sclf1  18881  prmirred  19064  cygznlem3  19138  frlmsslsp  19352  frlmlbs  19353  frlmup1  19354  mamuass  19425  dmatmul  19520  dmatsubcl  19521  dmatmulcl  19523  dmatcrng  19525  scmatcrng  19544  mdetunilem9  19643  pm2mpghm  19838  fvmptnn04ifb  19873  toponmre  20107  neiptopreu  20147  ordtbas  20206  txcls  20617  txlm  20661  qtoptop2  20712  qtoprest  20730  kqt0lem  20749  ptuncnv  20820  fmfnfmlem4  20970  alexsubALTlem2  21061  tgpmulg  21106  blin  21434  xmeter  21446  xmetresbl  21450  dscmet  21585  nmdvr  21671  metnrmlem3  21876  metnrmlem3OLD  21891  icccvx  21976  bndth  21984  htpycc  22009  pcohtpylem  22048  pi1blem  22068  lmmbrf  22230  iscfil2  22234  iscau4  22247  minveclem7  22375  minveclem7OLD  22387  elovolm  22426  dyaddisjlem  22551  ismbfd  22594  itg1mulc  22660  dvlip  22943  dvcvx  22970  plypf1  23164  eff1olem  23495  logccv  23606  lawcos  23743  sqff1o  24107  dvdsppwf1o  24113  dvdsflf1o  24114  fsumdvdsmul  24122  sgmmul  24127  fsumvma  24139  bposlem6  24215  lgsdchr  24274  rpvmasum2  24348  pntpbnd1  24422  ostthlem1  24463  tgbtwntriv2  24529  ercgrg  24560  hlpasch  24796  colhp  24810  colinearalglem4  24937  axlowdimlem15  24984  axcontlem7  24998  axcontlem8  24999  axcontlem10  25001  spthonepeq  25315  usgra2adedgspth  25339  usgra2adedgwlk  25340  usgra2adedgwlkon  25341  numclwlk1lem2f1  25820  grpolcan  25959  isgrp2d  25961  nvmf  26265  nvsubadd  26274  sspmval  26370  sspival  26375  nmosetre  26403  sspph  26494  minvecolem7  26523  minvecolem7OLD  26533  hiassdi  26742  shscli  26968  fh1  27269  fh2  27270  cm2j  27271  chscllem2  27289  spansncvi  27303  5oalem2  27306  adjsym  27484  nmopsetretALT  27514  nmfnsetre  27528  cnvadj  27543  cnvunop  27569  unoplin  27571  hmoplin  27593  lnopmi  27651  hmops  27671  hmopm  27672  nmcexi  27677  adjlnop  27737  adjmul  27743  adjadd  27744  opsqrlem1  27791  mdsl0  27961  ssmd2  27963  mdexchi  27986  superpos  28005  chrelat2i  28016  atcvatlem  28036  atcvati  28037  chirredlem1  28041  chirredi  28045  atcvat3i  28047  atcvat4i  28048  mdsymlem3  28056  mdsymlem5  28058  cdj3lem2b  28088  isoun  28284  xrge0infss  28346  xrge0infssOLD  28347  ddemeas  29067  bnj1145  29810  subfacp1lem3  29913  subfacp1lem5  29915  ghomf1olem  30320  frind  30488  sltres  30558  nodenselem6  30580  nodenselem7  30581  nodense  30583  nofulllem5  30600  btwnconn1lem12  30870  colinbtwnle  30890  broutsideof2  30894  lineelsb2  30920  nn0prpwlem  30983  neibastop2lem  31021  tailfb  31038  onsuct0  31106  finxpreclem2  31746  poimirlem4  31908  poimirlem26  31930  poimirlem27  31931  poimirlem31  31935  heicant  31939  mblfinlem2  31942  mblfinlem3  31943  ismblfin  31945  ftc1anclem5  31985  ftc1anclem6  31986  ftc1anc  31989  sdclem1  32036  seqpo  32040  sstotbnd  32071  cntotbnd  32092  ismtycnv  32098  ismtyres  32104  heibor  32117  exidreslem  32139  ghomdiv  32146  grpokerinj  32147  rngohomco  32177  rngoisoco  32185  idlsubcl  32220  divrngidl  32225  ispridl2  32235  ispridlc  32267  riotasv3d  32501  omllaw3  32780  omlfh1N  32793  hlrelat2  32937  cvratlem  32955  cvrat  32956  cvrat3  32976  cvrat4  32977  ps-2  33012  elpaddn0  33334  paddss12  33353  pmodlem2  33381  cdleme0cq  33750  cdlemeg49lebilem  34075  cdleme50eq  34077  tendoeq2  34310  tendoex  34511  diameetN  34593  diainN  34594  dvhopN  34653  djajN  34674  dihmeetcl  34882  mapdheq2  35266  fphpdo  35629  pell1234qrne0  35669  pell14qrgt0  35675  pell1qrge1  35686  monotoddzzfi  35760  expmordi  35765  jm2.18  35813  wepwsolem  35870  dnnumch3  35875  dnwech  35876  kelac1  35891  kercvrlsm  35911  gsumws3  36618  gsumws4  36619  cncmpmax  37326  fiiuncl  37379  mullimc  37636  mullimcf  37643  idlimc  37646  limclner  37672  fperdvper  37730  ioodvbdlimc1lem2  37744  ioodvbdlimc1lem2OLD  37746  ioodvbdlimc2lem  37748  ioodvbdlimc2lemOLD  37749  dvnprodlem1  37761  stoweidlem27  37827  stoweidlem48  37849  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem63  37973  fourierdlem65  37975  sge0iunmptlemfi  38163  sge0rpcpnf  38171  iundjiun  38206  psmeasure  38217  ovnsubaddlem2  38297  hoidmvle  38326  icceuelpart  38620  usgra2adedglem1  39290  mgmhmpropd  39405  subsubmgm  39417  srhmsubc  39698  srhmsubcALTV  39717
  Copyright terms: Public domain W3C validator