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

Theorem adantrl 713
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 459 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan2 472 1  |-  ( (
ph  /\  ( th  /\  ps ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  ad2ant2l  743  ad2ant2rl  746  consensus  957  cases2  969  3ad2antr2  1160  3ad2antr3  1161  ordelord  4814  foco  5713  isocnv  6127  isores2  6130  f1oiso2  6149  offval  6446  ordsucun  6559  opabex2  6637  xp2nd  6730  1stconst  6787  2ndconst  6788  smoord  6954  tfrlem9  6972  tfrlem11  6975  oaass  7128  omordi  7133  omwordri  7139  odi  7146  oewordri  7159  nnawordi  7188  nnmordi  7198  dom2lem  7474  fundmen  7508  sbthlem9  7554  mapen  7600  mapunen  7605  ssenen  7610  domfi  7657  mapfien  7782  inf3lem6  7964  mapfienOLD  8051  r1val1  8117  rankval3b  8157  numacn  8343  infxpabs  8505  infxp  8508  cfsmolem  8563  infpssrlem4  8599  fin23lem27  8621  isf34lem4  8670  hsmexlem2  8720  axdc3lem2  8744  axdc3lem4  8746  iundom2g  8828  gchen1  8914  fpwwe2lem7  8925  fpwwe2lem11  8929  fpwwe2lem12  8930  prlem936  9336  muladd  9907  leord1  9997  eqord1  9998  ltord2  9999  leord2  10000  eqord2  10001  divadddiv  10176  ltmul12a  10315  lemul12b  10316  supmullem1  10425  cju  10448  zextlt  10854  zmax  11098  xrre  11291  supxr  11425  ixxdisj  11465  iooshf  11524  icodisj  11566  ioojoin  11572  iccshftr  11575  iccshftl  11577  iccdil  11579  icccntr  11581  iccf1o  11585  fzaddel  11640  fzsubel  11641  modadd1  11934  modmul1  11943  seqcaopr  12047  expsub  12116  sqlecan  12177  facndiv  12268  hashss  12378  hashfacen  12407  hashf1lem1  12408  brfi1uzind  12436  swrdccatin12lem2b  12622  2cshwcshw  12704  resqrex  13086  fprodeq0  13781  hashdvds  14307  eulerthlem2  14314  pceu  14372  pcqcl  14382  infpnlem1  14430  4sqlem11  14475  ramcl  14549  imasvscafn  14944  invfun  15170  initoeu2lem2  15411  catcisolem  15502  funcestrcsetclem8  15533  fullestrcsetc  15537  embedsetcestrclem  15543  funcsetcestrclem8  15548  fullsetcestrc  15552  prfcl  15589  prf1st  15590  prf2nd  15591  1st2ndprf  15592  curfuncf  15624  ipodrsfi  15910  mhmpropd  16089  subsubm  16105  pwsdiagmhm  16117  gsumccat  16126  frmdgsum  16147  grplcan  16219  grplmulf1o  16229  mulgsubcl  16273  subsubg  16341  eqger  16368  resghm  16400  conjghm  16414  orbsta  16468  psgnunilem2  16637  odmulg  16695  sylow2a  16756  sylow3lem1  16764  lsmssv  16780  pj1ghm  16838  frgpup1  16910  ghmplusg  16969  subsubrg  17568  issrngd  17623  lmhmco  17802  lmhmf1o  17805  lmhmima  17806  lmhmpreima  17807  reslmhm  17811  pwsdiaglmhm  17816  pwssplit2  17819  pwssplit3  17820  pj1lmhm  17859  lspdisj  17884  issubassa2  18107  psrbagconf1o  18139  evlslem2  18293  evlslem1  18297  ply1sclf1  18443  prmirred  18625  cygznlem3  18699  frlmsslsp  18916  frlmlbs  18917  frlmup1  18918  mamuass  18989  dmatmul  19084  dmatsubcl  19085  dmatmulcl  19087  dmatcrng  19089  scmatcrng  19108  mdetunilem9  19207  pm2mpghm  19402  fvmptnn04ifb  19437  istps2OLD  19507  toponmre  19680  neiptopreu  19720  ordtbas  19779  txcls  20190  txlm  20234  qtoptop2  20285  qtoprest  20303  kqt0lem  20322  ptuncnv  20393  fmfnfmlem4  20543  alexsubALTlem2  20633  tgpmulg  20677  blin  21009  xmeter  21021  xmetresbl  21025  dscmet  21178  nmdvr  21264  metnrmlem3  21450  icccvx  21535  bndth  21543  htpycc  21565  pcohtpylem  21604  pi1blem  21624  lmmbrf  21786  iscfil2  21790  iscau4  21803  minveclem7  21935  elovolm  21971  dyaddisjlem  22089  ismbfd  22132  itg1mulc  22196  dvlip  22479  dvcvx  22506  plypf1  22694  eff1olem  23020  logccv  23131  lawcos  23266  sqff1o  23573  dvdsppwf1o  23579  dvdsflf1o  23580  fsumdvdsmul  23588  sgmmul  23593  fsumvma  23605  bposlem6  23681  lgsdchr  23740  rpvmasum2  23814  pntpbnd1  23888  ostthlem1  23929  tgbtwntriv2  23998  ercgrg  24028  colinearalglem4  24333  axlowdimlem15  24380  axcontlem7  24394  axcontlem8  24395  axcontlem10  24397  spthonepeq  24710  usgra2adedgspth  24734  usgra2adedgwlk  24735  usgra2adedgwlkon  24736  numclwlk1lem2f1  25215  grpolcan  25352  isgrp2d  25354  nvmf  25658  nvsubadd  25667  sspmval  25763  sspival  25768  nmosetre  25796  sspph  25887  minvecolem7  25916  hiassdi  26125  shscli  26352  fh1  26653  fh2  26654  cm2j  26655  chscllem2  26673  spansncvi  26687  5oalem2  26690  adjsym  26868  nmopsetretALT  26898  nmfnsetre  26912  cnvadj  26927  cnvunop  26953  unoplin  26955  hmoplin  26977  lnopmi  27035  hmops  27055  hmopm  27056  nmcexi  27061  adjlnop  27121  adjmul  27127  adjadd  27128  opsqrlem1  27175  mdsl0  27345  ssmd2  27347  mdexchi  27370  superpos  27389  chrelat2i  27400  atcvatlem  27420  atcvati  27421  chirredlem1  27425  chirredi  27429  atcvat3i  27431  atcvat4i  27432  mdsymlem3  27440  mdsymlem5  27442  cdj3lem2b  27472  isoun  27667  xrge0infss  27730  ddemeas  28364  subfacp1lem3  28815  subfacp1lem5  28817  ghomf1olem  29223  wfi  29452  frind  29488  wfrlem9  29516  sltres  29589  nodenselem6  29611  nodenselem7  29612  nodense  29614  nofulllem5  29631  btwnconn1lem12  29901  colinbtwnle  29921  broutsideof2  29925  lineelsb2  29951  onsuct0  30059  supadd  30207  heicant  30214  mblfinlem2  30217  mblfinlem3  30218  ismblfin  30220  ftc1anclem5  30260  ftc1anclem6  30261  ftc1anc  30264  nn0prpwlem  30306  neibastop2lem  30344  tailfb  30361  sdclem1  30402  seqpo  30406  sstotbnd  30437  cntotbnd  30458  ismtycnv  30464  ismtyres  30470  heibor  30483  exidreslem  30505  ghomdiv  30512  grpokerinj  30513  rngohomco  30543  rngoisoco  30551  idlsubcl  30586  divrngidl  30591  ispridl2  30601  ispridlc  30633  fphpdo  30916  pell1234qrne0  30954  pell14qrgt0  30960  pell1qrge1  30971  monotoddzzfi  31043  expmordi  31048  jm2.18  31096  wepwsolem  31153  dnnumch3  31159  dnwech  31160  kelac1  31175  kercvrlsm  31195  lcmdvds  31382  cncmpmax  31574  mullimc  31788  mullimcf  31795  idlimc  31798  limclner  31823  fperdvper  31881  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  dvnprodlem1  31909  stoweidlem27  31975  stoweidlem48  31996  fourierdlem42  32097  fourierdlem63  32118  fourierdlem65  32120  usgra2adedglem1  32674  mgmhmpropd  32791  subsubmgm  32803  srhmsubc  33084  srhmsubcALTV  33103  bnj1145  34396  riotasv3d  35104  omllaw3  35383  omlfh1N  35396  hlrelat2  35540  cvratlem  35558  cvrat  35559  cvrat3  35579  cvrat4  35580  ps-2  35615  elpaddn0  35937  paddss12  35956  pmodlem2  35984  cdleme0cq  36353  cdlemeg49lebilem  36678  cdleme50eq  36680  tendoeq2  36913  tendoex  37114  diameetN  37196  diainN  37197  dvhopN  37256  djajN  37277  dihmeetcl  37485  mapdheq2  37869
  Copyright terms: Public domain W3C validator