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  957  cases2  970  3ad2antr2  1162  3ad2antr3  1163  ordelord  4900  foco  5803  isocnv  6212  isores2  6215  f1oiso2  6234  offval  6529  ordsucun  6638  opabex2  6719  xp2nd  6812  1stconst  6868  2ndconst  6869  smoord  7033  tfrlem9  7051  tfrlem11  7054  oaass  7207  omordi  7212  omwordri  7218  odi  7225  oewordri  7238  nnawordi  7267  nnmordi  7277  dom2lem  7552  fundmen  7586  sbthlem9  7632  mapen  7678  mapunen  7683  ssenen  7688  domfi  7738  mapfien  7863  inf3lem6  8046  mapfienOLD  8134  r1val1  8200  rankval3b  8240  numacn  8426  infxpabs  8588  infxp  8591  cfsmolem  8646  infpssrlem4  8682  fin23lem27  8704  isf34lem4  8753  hsmexlem2  8803  axdc3lem2  8827  axdc3lem4  8829  iundom2g  8911  gchen1  8999  fpwwe2lem7  9010  fpwwe2lem11  9014  fpwwe2lem12  9015  prlem936  9421  muladd  9985  leord1  10076  eqord1  10077  ltord2  10078  leord2  10079  eqord2  10080  divadddiv  10255  ltmul12a  10394  lemul12b  10395  supmullem1  10505  cju  10528  zextlt  10931  zmax  11175  xrre  11366  supxr  11500  ixxdisj  11540  iooshf  11599  icodisj  11641  ioojoin  11647  iccshftr  11650  iccshftl  11652  iccdil  11654  icccntr  11656  iccf1o  11660  fzaddel  11714  fzsubel  11715  modadd1  11996  modmul1  12003  seqcaopr  12107  expsub  12175  sqlecan  12236  facndiv  12328  hashss  12433  hashfacen  12463  hashf1lem1  12464  brfi1uzind  12492  swrdccatin12lem2b  12668  2cshwcshw  12750  resqrex  13041  hashdvds  14157  eulerthlem2  14164  pceu  14222  pcqcl  14232  infpnlem1  14280  4sqlem11  14325  ramcl  14399  imasvscafn  14785  invfun  15012  catcisolem  15284  prfcl  15323  prf1st  15324  prf2nd  15325  1st2ndprf  15326  curfuncf  15358  ipodrsfi  15643  mhmpropd  15780  subsubm  15795  pwsdiagmhm  15807  gsumccat  15829  frmdgsum  15850  grplcan  15900  grplmulf1o  15910  mulgsubcl  15953  subsubg  16016  eqger  16043  resghm  16075  conjghm  16089  orbsta  16143  psgnunilem2  16313  odmulg  16371  sylow2a  16432  sylow3lem1  16440  lsmssv  16456  pj1ghm  16514  frgpup1  16586  ghmplusg  16642  subsubrg  17235  issrngd  17290  lmhmco  17469  lmhmf1o  17472  lmhmima  17473  lmhmpreima  17474  reslmhm  17478  pwsdiaglmhm  17483  pwssplit2  17486  pwssplit3  17487  pj1lmhm  17526  lspdisj  17551  issubassa2  17762  psrbagconf1o  17794  evlslem2  17948  evlslem1  17952  ply1sclf1  18098  prmirred  18289  prmirredOLD  18292  cygznlem3  18372  frlmsslsp  18593  frlmsslspOLD  18594  frlmlbs  18595  frlmup1  18596  mamuass  18668  dmatmul  18763  dmatsubcl  18764  dmatmulcl  18766  dmatcrng  18768  scmatcrng  18787  mdetunilem9  18886  pm2mpghm  19081  fvmptnn04ifb  19116  istps2OLD  19186  toponmre  19357  neiptopreu  19397  ordtbas  19456  txcls  19837  txlm  19881  qtoptop2  19932  qtoprest  19950  kqt0lem  19969  ptuncnv  20040  fmfnfmlem4  20190  alexsubALTlem2  20280  tgpmulg  20324  blin  20656  xmeter  20668  xmetresbl  20672  dscmet  20825  nmdvr  20911  metnrmlem3  21097  icccvx  21182  bndth  21190  htpycc  21212  pcohtpylem  21251  pi1blem  21271  lmmbrf  21433  iscfil2  21437  iscau4  21450  minveclem7  21582  elovolm  21618  dyaddisjlem  21736  ismbfd  21779  itg1mulc  21843  dvlip  22126  dvcvx  22153  plypf1  22341  eff1olem  22665  logccv  22769  lawcos  22873  sqff1o  23181  dvdsppwf1o  23187  dvdsflf1o  23188  fsumdvdsmul  23196  sgmmul  23201  fsumvma  23213  bposlem6  23289  lgsdchr  23348  rpvmasum2  23422  pntpbnd1  23496  ostthlem1  23537  tgbtwntriv2  23603  ercgrg  23633  colinearalglem4  23885  axlowdimlem15  23932  axcontlem7  23946  axcontlem8  23947  axcontlem10  23949  spthonepeq  24262  usgra2adedgspth  24286  usgra2adedgwlk  24287  usgra2adedgwlkon  24288  numclwlk1lem2f1  24768  grpolcan  24908  isgrp2d  24910  nvmf  25214  nvsubadd  25223  sspmval  25319  sspival  25324  nmosetre  25352  sspph  25443  minvecolem7  25472  hiassdi  25681  shscli  25908  fh1  26209  fh2  26210  cm2j  26211  chscllem2  26229  spansncvi  26243  5oalem2  26246  adjsym  26425  nmopsetretALT  26455  nmfnsetre  26469  cnvadj  26484  cnvunop  26510  unoplin  26512  hmoplin  26534  lnopmi  26592  hmops  26612  hmopm  26613  nmcexi  26618  adjlnop  26678  adjmul  26684  adjadd  26685  opsqrlem1  26732  mdsl0  26902  ssmd2  26904  mdexchi  26927  superpos  26946  chrelat2i  26957  atcvatlem  26977  atcvati  26978  chirredlem1  26982  chirredi  26986  atcvat3i  26988  atcvat4i  26989  mdsymlem3  26997  mdsymlem5  26999  cdj3lem2b  27029  isoun  27189  xrge0infss  27245  ddemeas  27845  afsval  28188  subfacp1lem3  28263  subfacp1lem5  28265  ghomf1olem  28506  fprodeq0  28679  wfi  28861  frind  28897  wfrlem9  28925  sltres  28998  nodenselem6  29020  nodenselem7  29021  nodense  29023  nofulllem5  29040  btwnconn1lem12  29322  colinbtwnle  29342  broutsideof2  29346  lineelsb2  29372  onsuct0  29480  supadd  29616  heicant  29624  mblfinlem2  29627  mblfinlem3  29628  ismblfin  29630  ftc1anclem5  29669  ftc1anclem6  29670  ftc1anc  29673  nn0prpwlem  29715  neibastop2lem  29779  tailfb  29796  sdclem1  29837  seqpo  29841  sstotbnd  29872  cntotbnd  29893  ismtycnv  29899  ismtyres  29905  heibor  29918  exidreslem  29940  ghomdiv  29947  grpokerinj  29948  rngohomco  29978  rngoisoco  29986  idlsubcl  30021  divrngidl  30026  ispridl2  30036  ispridlc  30068  fphpdo  30353  pell1234qrne0  30391  pell14qrgt0  30397  pell1qrge1  30408  monotoddzzfi  30480  expmordi  30485  jm2.18  30534  wepwsolem  30591  dnnumch3  30597  dnwech  30598  kelac1  30613  kercvrlsm  30633  lcmdvds  30814  cncmpmax  30985  mullimc  31158  mullimcf  31165  idlimc  31168  limclner  31193  fperdvper  31248  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  stoweidlem27  31327  stoweidlem48  31348  fourierdlem42  31449  fourierdlem63  31470  fourierdlem65  31472  usgra2adedglem1  31825  bnj1145  33128  riotasv3d  33763  omllaw3  34042  omlfh1N  34055  hlrelat2  34199  cvratlem  34217  cvrat  34218  cvrat3  34238  cvrat4  34239  ps-2  34274  elpaddn0  34596  paddss12  34615  pmodlem2  34643  cdleme0cq  35011  cdlemeg49lebilem  35335  cdleme50eq  35337  tendoeq2  35570  tendoex  35771  diameetN  35853  diainN  35854  dvhopN  35913  djajN  35934  dihmeetcl  36142  mapdheq2  36526
  Copyright terms: Public domain W3C validator