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

Theorem adantrl 715
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 461 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan2 474 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  745  ad2ant2rl  748  consensus  950  3ad2antr2  1154  3ad2antr3  1155  ordelord  4839  foco  5728  isocnv  6120  isores2  6123  f1oiso2  6142  offval  6427  ordsucun  6536  opabex2  6616  xp2nd  6707  1stconst  6761  2ndconst  6762  smoord  6926  tfrlem9  6944  tfrlem11  6947  oaass  7100  omordi  7105  omwordri  7111  odi  7118  oewordri  7131  nnawordi  7160  nnmordi  7170  dom2lem  7449  fundmen  7483  sbthlem9  7529  mapen  7575  mapunen  7580  ssenen  7585  domfi  7635  mapfien  7758  inf3lem6  7940  mapfienOLD  8028  r1val1  8094  rankval3b  8134  numacn  8320  infxpabs  8482  infxp  8485  cfsmolem  8540  infpssrlem4  8576  fin23lem27  8598  isf34lem4  8647  hsmexlem2  8697  axdc3lem2  8721  axdc3lem4  8723  iundom2g  8805  gchen1  8893  fpwwe2lem7  8904  fpwwe2lem11  8908  fpwwe2lem12  8909  prlem936  9317  muladd  9878  leord1  9968  eqord1  9969  ltord2  9970  leord2  9971  eqord2  9972  divadddiv  10147  ltmul12a  10286  lemul12b  10287  supmullem1  10397  cju  10419  zextlt  10817  zmax  11051  xrre  11242  supxr  11376  ixxdisj  11416  iooshf  11475  icodisj  11511  ioojoin  11517  iccshftr  11520  iccshftl  11522  iccdil  11524  icccntr  11526  iccf1o  11530  fzaddel  11594  fzsubel  11595  modadd1  11846  modmul1  11853  seqcaopr  11944  expsub  12012  sqlecan  12073  facndiv  12165  hashss  12268  hashfacen  12309  hashf1lem1  12310  brfi1uzind  12321  swrdccatin12lem2b  12479  resqrex  12842  hashdvds  13952  eulerthlem2  13959  pceu  14015  pcqcl  14025  infpnlem1  14073  4sqlem11  14118  ramcl  14192  imasvscafn  14577  invfun  14804  catcisolem  15076  prfcl  15115  prf1st  15116  prf2nd  15117  1st2ndprf  15118  curfuncf  15150  ipodrsfi  15435  mhmpropd  15572  subsubm  15587  pwsdiagmhm  15599  gsumccat  15621  frmdgsum  15642  grplcan  15692  grplmulf1o  15702  mulgsubcl  15743  subsubg  15806  eqger  15833  resghm  15865  conjghm  15879  orbsta  15933  psgnunilem2  16103  odmulg  16161  sylow2a  16222  sylow3lem1  16230  lsmssv  16246  pj1ghm  16304  frgpup1  16376  ghmplusg  16432  subsubrg  16997  issrngd  17052  lmhmco  17230  lmhmf1o  17233  lmhmima  17234  lmhmpreima  17235  reslmhm  17239  pwsdiaglmhm  17244  pwssplit2  17247  pwssplit3  17248  pj1lmhm  17287  lspdisj  17312  issubassa2  17521  psrbagconf1o  17550  evlslem2  17704  evlslem1  17708  ply1sclf1  17850  prmirred  18028  prmirredOLD  18031  cygznlem3  18111  frlmsslsp  18332  frlmsslspOLD  18333  frlmlbs  18334  frlmup1  18335  mamuass  18415  mdetunilem9  18542  istps2OLD  18642  toponmre  18813  neiptopreu  18853  ordtbas  18912  txcls  19293  txlm  19337  qtoptop2  19388  qtoprest  19406  kqt0lem  19425  ptuncnv  19496  fmfnfmlem4  19646  alexsubALTlem2  19736  tgpmulg  19780  blin  20112  xmeter  20124  xmetresbl  20128  dscmet  20281  nmdvr  20367  metnrmlem3  20553  icccvx  20638  bndth  20646  htpycc  20668  pcohtpylem  20707  pi1blem  20727  lmmbrf  20889  iscfil2  20893  iscau4  20906  minveclem7  21038  elovolm  21074  dyaddisjlem  21191  ismbfd  21234  itg1mulc  21298  dvlip  21581  dvcvx  21608  plypf1  21796  eff1olem  22120  logccv  22224  lawcos  22328  sqff1o  22636  dvdsppwf1o  22642  dvdsflf1o  22643  fsumdvdsmul  22651  sgmmul  22656  fsumvma  22668  bposlem6  22744  lgsdchr  22803  rpvmasum2  22877  pntpbnd1  22951  ostthlem1  22992  tgbtwntriv2  23058  ercgrg  23088  colinearalglem4  23290  axlowdimlem15  23337  axcontlem7  23351  axcontlem8  23352  axcontlem10  23354  spthonepeq  23621  grpolcan  23855  isgrp2d  23857  nvmf  24161  nvsubadd  24170  sspmval  24266  sspival  24271  nmosetre  24299  sspph  24390  minvecolem7  24419  hiassdi  24628  shscli  24855  fh1  25156  fh2  25157  cm2j  25158  chscllem2  25176  spansncvi  25190  5oalem2  25193  adjsym  25372  nmopsetretALT  25402  nmfnsetre  25416  cnvadj  25431  cnvunop  25457  unoplin  25459  hmoplin  25481  lnopmi  25539  hmops  25559  hmopm  25560  nmcexi  25565  adjlnop  25625  adjmul  25631  adjadd  25632  opsqrlem1  25679  mdsl0  25849  ssmd2  25851  mdexchi  25874  superpos  25893  chrelat2i  25904  atcvatlem  25924  atcvati  25925  chirredlem1  25929  chirredi  25933  atcvat3i  25935  atcvat4i  25936  mdsymlem3  25944  mdsymlem5  25946  cdj3lem2b  25976  isoun  26131  xrge0infss  26187  ddemeas  26786  afsval  27129  subfacp1lem3  27204  subfacp1lem5  27206  ghomf1olem  27447  fprodeq0  27620  wfi  27802  frind  27838  wfrlem9  27866  sltres  27939  nodenselem6  27961  nodenselem7  27962  nodense  27964  nofulllem5  27981  btwnconn1lem12  28263  colinbtwnle  28283  broutsideof2  28287  lineelsb2  28313  onsuct0  28421  supadd  28556  heicant  28564  mblfinlem2  28567  mblfinlem3  28568  ismblfin  28570  ftc1anclem5  28609  ftc1anclem6  28610  ftc1anc  28613  nn0prpwlem  28655  neibastop2lem  28719  tailfb  28736  sdclem1  28777  seqpo  28781  sstotbnd  28812  cntotbnd  28833  ismtycnv  28839  ismtyres  28845  heibor  28858  exidreslem  28880  ghomdiv  28887  grpokerinj  28888  rngohomco  28918  rngoisoco  28926  idlsubcl  28961  divrngidl  28966  ispridl2  28976  ispridlc  29008  fphpdo  29294  pell1234qrne0  29332  pell14qrgt0  29338  pell1qrge1  29349  monotoddzzfi  29421  expmordi  29426  jm2.18  29475  wepwsolem  29532  dnnumch3  29538  dnwech  29539  kelac1  29554  kercvrlsm  29574  cncmpmax  29892  stoweidlem27  29960  stoweidlem48  29981  usgra2adedgspth  30443  usgra2adedgwlk  30444  usgra2adedgwlkon  30445  usgra2adedglem1  30446  cshwlemma1  30627  numclwlk1lem2f1  30825  dmatmul  31030  pmattomply1ghm  31270  fvmptnn04ifb  31305  bnj1145  32284  riotasv3d  32917  omllaw3  33196  omlfh1N  33209  hlrelat2  33353  cvratlem  33371  cvrat  33372  cvrat3  33392  cvrat4  33393  ps-2  33428  elpaddn0  33750  paddss12  33769  pmodlem2  33797  cdleme0cq  34165  cdlemeg49lebilem  34489  cdleme50eq  34491  tendoeq2  34724  tendoex  34925  diameetN  35007  diainN  35008  dvhopN  35067  djajN  35088  dihmeetcl  35296  mapdheq2  35680
  Copyright terms: Public domain W3C validator