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  7052  smoord  7092  tfrlem9  7111  tfrlem11  7114  oaass  7270  omordi  7275  omwordri  7281  odi  7288  oewordri  7301  nnawordi  7330  nnmordi  7340  dom2lem  7616  fundmen  7650  sbthlem9  7696  mapen  7742  mapunen  7747  ssenen  7752  domfi  7799  mapfien  7927  inf3lem6  8138  r1val1  8256  rankval3b  8296  numacn  8478  infxpabs  8640  infxp  8643  cfsmolem  8698  infpssrlem4  8734  fin23lem27  8756  isf34lem4  8805  hsmexlem2  8855  axdc3lem2  8879  axdc3lem4  8881  iundom2g  8963  gchen1  9049  fpwwe2lem7  9060  fpwwe2lem11  9064  fpwwe2lem12  9065  prlem936  9471  muladd  10050  leord1  10140  eqord1  10141  ltord2  10142  leord2  10143  eqord2  10144  divadddiv  10321  ltmul12a  10460  lemul12b  10461  supadd  10575  supmullem1  10577  cju  10605  zextlt  11010  zmax  11261  xrre  11464  supxr  11598  ixxdisj  11650  iooshf  11713  icodisj  11755  ioojoin  11761  iccshftr  11764  iccshftl  11766  iccdil  11768  icccntr  11770  iccf1o  11774  fzaddel  11831  fzsubel  11832  modadd1  12131  modmul1  12140  seqcaopr  12247  expsub  12317  sqlecan  12378  facndiv  12470  hashss  12583  hashfacen  12612  hashf1lem1  12613  brfi1uzind  12641  swrdccatin12lem2b  12827  2cshwcshw  12909  resqrex  13293  fprodeq0  14007  lcmdvds  14538  hashdvds  14683  eulerthlem2  14690  pceu  14750  pcqcl  14760  infpnlem1  14808  4sqlem11  14853  ramcl  14941  prmgaplem5  14979  imasvscafn  15385  invfun  15611  initoeu2lem2  15852  catcisolem  15943  funcestrcsetclem8  15974  fullestrcsetc  15978  embedsetcestrclem  15984  funcsetcestrclem8  15989  fullsetcestrc  15993  prfcl  16030  prf1st  16031  prf2nd  16032  1st2ndprf  16033  curfuncf  16065  ipodrsfi  16351  mhmpropd  16530  subsubm  16546  pwsdiagmhm  16558  gsumccat  16567  frmdgsum  16588  grplcan  16660  grplmulf1o  16670  mulgsubcl  16714  subsubg  16782  eqger  16809  resghm  16841  conjghm  16855  orbsta  16909  psgnunilem2  17078  odmulg  17136  sylow2a  17197  sylow3lem1  17205  lsmssv  17221  pj1ghm  17279  frgpup1  17351  ghmplusg  17410  subsubrg  17960  issrngd  18015  lmhmco  18192  lmhmf1o  18195  lmhmima  18196  lmhmpreima  18197  reslmhm  18201  pwsdiaglmhm  18206  pwssplit2  18209  pwssplit3  18210  pj1lmhm  18249  lspdisj  18274  issubassa2  18495  psrbagconf1o  18524  evlslem2  18661  evlslem1  18664  ply1sclf1  18808  prmirred  18988  cygznlem3  19062  frlmsslsp  19276  frlmlbs  19277  frlmup1  19278  mamuass  19349  dmatmul  19444  dmatsubcl  19445  dmatmulcl  19447  dmatcrng  19449  scmatcrng  19468  mdetunilem9  19567  pm2mpghm  19762  fvmptnn04ifb  19797  toponmre  20031  neiptopreu  20071  ordtbas  20130  txcls  20541  txlm  20585  qtoptop2  20636  qtoprest  20654  kqt0lem  20673  ptuncnv  20744  fmfnfmlem4  20894  alexsubALTlem2  20985  tgpmulg  21030  blin  21358  xmeter  21370  xmetresbl  21374  dscmet  21509  nmdvr  21595  metnrmlem3  21780  icccvx  21865  bndth  21873  htpycc  21895  pcohtpylem  21934  pi1blem  21954  lmmbrf  22116  iscfil2  22120  iscau4  22133  minveclem7  22261  elovolm  22297  dyaddisjlem  22421  ismbfd  22464  itg1mulc  22530  dvlip  22813  dvcvx  22840  plypf1  23025  eff1olem  23353  logccv  23464  lawcos  23601  sqff1o  23963  dvdsppwf1o  23969  dvdsflf1o  23970  fsumdvdsmul  23978  sgmmul  23983  fsumvma  23995  bposlem6  24071  lgsdchr  24130  rpvmasum2  24204  pntpbnd1  24278  ostthlem1  24319  tgbtwntriv2  24385  ercgrg  24415  colhp  24659  colinearalglem4  24776  axlowdimlem15  24823  axcontlem7  24837  axcontlem8  24838  axcontlem10  24840  spthonepeq  25153  usgra2adedgspth  25177  usgra2adedgwlk  25178  usgra2adedgwlkon  25179  numclwlk1lem2f1  25658  grpolcan  25797  isgrp2d  25799  nvmf  26103  nvsubadd  26112  sspmval  26208  sspival  26213  nmosetre  26241  sspph  26332  minvecolem7  26361  hiassdi  26570  shscli  26796  fh1  27097  fh2  27098  cm2j  27099  chscllem2  27117  spansncvi  27131  5oalem2  27134  adjsym  27312  nmopsetretALT  27342  nmfnsetre  27356  cnvadj  27371  cnvunop  27397  unoplin  27399  hmoplin  27421  lnopmi  27479  hmops  27499  hmopm  27500  nmcexi  27505  adjlnop  27565  adjmul  27571  adjadd  27572  opsqrlem1  27619  mdsl0  27789  ssmd2  27791  mdexchi  27814  superpos  27833  chrelat2i  27844  atcvatlem  27864  atcvati  27865  chirredlem1  27869  chirredi  27873  atcvat3i  27875  atcvat4i  27876  mdsymlem3  27884  mdsymlem5  27886  cdj3lem2b  27916  isoun  28113  xrge0infss  28172  ddemeas  28889  bnj1145  29581  subfacp1lem3  29684  subfacp1lem5  29686  ghomf1olem  30091  frind  30259  sltres  30329  nodenselem6  30351  nodenselem7  30352  nodense  30354  nofulllem5  30371  btwnconn1lem12  30641  colinbtwnle  30661  broutsideof2  30665  lineelsb2  30691  nn0prpwlem  30754  neibastop2lem  30792  tailfb  30809  onsuct0  30877  poimirlem4  31638  poimirlem26  31660  poimirlem27  31661  poimirlem31  31665  heicant  31669  mblfinlem2  31672  mblfinlem3  31673  ismblfin  31675  ftc1anclem5  31715  ftc1anclem6  31716  ftc1anc  31719  sdclem1  31766  seqpo  31770  sstotbnd  31801  cntotbnd  31822  ismtycnv  31828  ismtyres  31834  heibor  31847  exidreslem  31869  ghomdiv  31876  grpokerinj  31877  rngohomco  31907  rngoisoco  31915  idlsubcl  31950  divrngidl  31955  ispridl2  31965  ispridlc  31997  riotasv3d  32231  omllaw3  32510  omlfh1N  32523  hlrelat2  32667  cvratlem  32685  cvrat  32686  cvrat3  32706  cvrat4  32707  ps-2  32742  elpaddn0  33064  paddss12  33083  pmodlem2  33111  cdleme0cq  33480  cdlemeg49lebilem  33805  cdleme50eq  33807  tendoeq2  34040  tendoex  34241  diameetN  34323  diainN  34324  dvhopN  34383  djajN  34404  dihmeetcl  34612  mapdheq2  34996  fphpdo  35359  pell1234qrne0  35397  pell14qrgt0  35403  pell1qrge1  35414  monotoddzzfi  35486  expmordi  35491  jm2.18  35539  wepwsolem  35596  dnnumch3  35601  dnwech  35602  kelac1  35617  kercvrlsm  35637  gsumws4  36276  cncmpmax  36983  fiiuncl  37038  mullimc  37258  mullimcf  37265  idlimc  37268  limclner  37294  fperdvper  37352  ioodvbdlimc1lem2  37366  ioodvbdlimc2lem  37368  dvnprodlem1  37380  stoweidlem27  37446  stoweidlem48  37468  fourierdlem42  37570  fourierdlem63  37591  fourierdlem65  37593  sge0iunmptlemfi  37779  iundjiun  37797  psmeasure  37808  icceuelpart  38130  usgra2adedglem1  38416  mgmhmpropd  38533  subsubmgm  38545  srhmsubc  38826  srhmsubcALTV  38845
  Copyright terms: Public domain W3C validator