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

Theorem adantrl 698
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 449 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan2 462 1  |-  ( (
ph  /\  ( th  /\  ps ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  ad2ant2l  728  ad2ant2rl  731  consensus  927  3ad2antr2  1124  3ad2antr3  1125  sbcom  2166  sbcomOLD  2167  ordelord  4605  ordsucun  4807  foco  5665  isocnv  6052  isores2  6055  f1oiso2  6074  offval  6314  xp2nd  6379  1stconst  6437  2ndconst  6438  riotasv3d  6600  riotasv3dOLD  6601  smoord  6629  tfrlem9  6648  tfrlem11  6651  oaass  6806  omordi  6811  omwordri  6817  odi  6824  oewordri  6837  nnawordi  6866  nnmordi  6876  dom2lem  7149  fundmen  7182  sbthlem9  7227  mapen  7273  mapunen  7278  ssenen  7283  domfi  7332  inf3lem6  7590  mapfien  7655  r1val1  7714  rankval3b  7754  numacn  7932  infxpabs  8094  infxp  8097  cfsmolem  8152  infpssrlem4  8188  fin23lem27  8210  isf34lem4  8259  hsmexlem2  8309  axdc3lem2  8333  axdc3lem4  8335  iundom2g  8417  gchen1  8502  fpwwe2lem7  8513  fpwwe2lem11  8517  fpwwe2lem12  8518  prlem936  8926  muladd  9468  leord1  9556  eqord1  9557  ltord2  9558  leord2  9559  eqord2  9560  divadddiv  9731  ltmul12a  9868  lemul12b  9869  supmullem1  9976  cju  9998  zextlt  10346  zmax  10573  xrre  10759  supxr  10893  ixxdisj  10933  iooshf  10991  icodisj  11024  ioojoin  11029  iccshftr  11032  iccshftl  11034  iccdil  11036  icccntr  11038  iccf1o  11041  fzaddel  11089  fzsubel  11090  modadd1  11280  modmul1  11281  seqcaopr  11362  expsub  11429  sqlecan  11489  facndiv  11581  hashfacen  11705  hashf1lem1  11706  brfi1uzind  11717  resqrex  12058  hashdvds  13166  eulerthlem2  13173  pceu  13222  pcqcl  13232  infpnlem1  13280  4sqlem11  13325  ramcl  13399  imasvscafn  13764  invfun  13991  catcisolem  14263  prfcl  14302  prf1st  14303  prf2nd  14304  1st2ndprf  14305  curfuncf  14337  ipodrsfi  14591  mhmpropd  14746  subsubm  14759  pwsdiagmhm  14770  gsumccat  14789  frmdgsum  14809  grplcan  14859  grplmulf1o  14867  mulgsubcl  14906  subsubg  14965  eqger  14992  resghm  15024  conjghm  15038  orbsta  15092  odmulg  15194  sylow2a  15255  sylow3lem1  15263  lsmssv  15279  pj1ghm  15337  frgpup1  15409  ghmplusg  15463  subsubrg  15896  issrngd  15951  lmhmco  16121  lmhmf1o  16124  lmhmima  16125  lmhmpreima  16126  reslmhm  16130  pwsdiaglmhm  16135  pj1lmhm  16174  lspdisj  16199  issubassa2  16405  psrbagconf1o  16441  evlslem2  16570  ply1sclf1  16682  prmirred  16777  cygznlem3  16852  istps2OLD  16988  toponmre  17159  neiptopreu  17199  ordtbas  17258  txcls  17638  txlm  17682  qtoptop2  17733  qtoprest  17751  kqt0lem  17770  ptuncnv  17841  fmfnfmlem4  17991  alexsubALTlem2  18081  tgpmulg  18125  blin  18453  xmeter  18465  xmetresbl  18469  dscmet  18622  nmdvr  18708  metnrmlem3  18893  icccvx  18977  bndth  18985  htpycc  19007  pcohtpylem  19046  pi1blem  19066  lmmbrf  19217  iscfil2  19221  iscau4  19234  minveclem7  19338  elovolm  19373  dyaddisjlem  19489  ismbfd  19534  itg1mulc  19598  dvlip  19879  dvcvx  19906  evlslem1  19938  plypf1  20133  eff1olem  20452  logccv  20556  lawcos  20660  sqff1o  20967  dvdsppwf1o  20973  dvdsflf1o  20974  fsumdvdsmul  20982  sgmmul  20987  fsumvma  20999  bposlem6  21075  lgsdchr  21134  rpvmasum2  21208  pntpbnd1  21282  ostthlem1  21323  spthonepeq  21589  grpolcan  21823  isgrp2d  21825  nvmf  22129  nvsubadd  22138  sspmval  22234  sspival  22239  nmosetre  22267  sspph  22358  minvecolem7  22387  hiassdi  22595  shscli  22821  fh1  23122  fh2  23123  cm2j  23124  chscllem2  23142  spansncvi  23156  5oalem2  23159  adjsym  23338  nmopsetretALT  23368  nmfnsetre  23382  cnvadj  23397  cnvunop  23423  unoplin  23425  hmoplin  23447  lnopmi  23505  hmops  23525  hmopm  23526  nmcexi  23531  adjlnop  23591  adjmul  23597  adjadd  23598  opsqrlem1  23645  mdsl0  23815  ssmd2  23817  mdexchi  23840  superpos  23859  chrelat2i  23870  atcvatlem  23890  atcvati  23891  chirredlem1  23895  chirredi  23899  atcvat3i  23901  atcvat4i  23902  mdsymlem3  23910  mdsymlem5  23912  cdj3lem2b  23942  isoun  24091  subfacp1lem3  24870  subfacp1lem5  24872  ghomf1olem  25107  fprodeq0  25301  wfi  25484  frind  25520  wfrlem9  25548  sltres  25621  nodenselem6  25643  nodenselem7  25644  nodense  25646  nofulllem5  25663  colinearalglem4  25850  axlowdimlem15  25897  axcontlem7  25911  axcontlem8  25912  axcontlem10  25914  btwnconn1lem12  26034  colinbtwnle  26054  broutsideof2  26058  lineelsb2  26084  onsuct0  26193  supadd  26240  mblfinlem2  26246  mblfinlem3  26247  ismblfin  26249  ftc1anclem5  26286  ftc1anclem6  26287  ftc1anc  26290  nn0prpwlem  26327  neibastop2lem  26391  tailfb  26408  sdclem1  26449  seqpo  26453  sstotbnd  26486  cntotbnd  26507  ismtycnv  26513  ismtyres  26519  heibor  26532  exidreslem  26554  ghomdiv  26561  grpokerinj  26562  rngohomco  26592  rngoisoco  26600  idlsubcl  26635  divrngidl  26640  ispridl2  26650  ispridlc  26682  fphpdo  26880  pell1234qrne0  26918  pell14qrgt0  26924  pell1qrge1  26935  monotoddzzfi  27007  expmordi  27012  jm2.18  27061  wepwsolem  27118  dnnumch3  27124  dnwech  27125  kelac1  27140  kercvrlsm  27160  pwssplit2  27168  pwssplit3  27169  frlmsslsp  27227  frlmlbs  27228  frlmup1  27229  psgnunilem2  27397  mamuass  27439  cncmpmax  27681  stoweidlem27  27754  stoweidlem48  27775  hashss  28180  swrdccatin12lem3b  28231  usgra2adedgspth  28341  usgra2adedgwlk  28342  usgra2adedgwlkon  28343  usgra2adedglem1  28344  bnj1145  29424  sbcomwAUX7  29650  sbcomOLD7  29817  omllaw3  30105  omlfh1N  30118  hlrelat2  30262  cvratlem  30280  cvrat  30281  cvrat3  30301  cvrat4  30302  ps-2  30337  elpaddn0  30659  paddss12  30678  pmodlem2  30706  cdleme0cq  31074  cdlemeg49lebilem  31398  cdleme50eq  31400  tendoeq2  31633  tendoex  31834  diameetN  31916  diainN  31917  dvhopN  31976  djajN  31997  dihmeetcl  32205  mapdheq2  32589
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator