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

Theorem 3adant3r3 1164
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3adant3r3  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )

Proof of Theorem 3adant3r3
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213expb 1154 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr3 1118 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  ressress  13489  plttr  14390  plelttr  14392  joinle  14413  meetle  14420  latjle12  14454  latlem12  14470  latledi  14481  latmlej11  14482  latmlej21  14484  latmlej22  14485  latjass  14487  latj12  14488  latj31  14491  ipopos  14549  latdisdlem  14578  ismndd  14682  imasmnd2  14695  imasmnd  14696  grpaddsubass  14841  grpsubsub4  14844  grpnpncan  14846  imasgrp2  14896  imasgrp  14897  frgp0  15355  cmn12  15395  abladdsub  15402  imasrng  15688  dvrass  15758  lss1  15978  islmhm2  16077  psrgrp  16425  psrlmod  16428  zntoslem  16800  ipdir  16833  t1sep  17396  mettri2  18332  xmetrtri  18346  xmetrtri2  18347  pi1grplem  19035  dchrabl  20999  grpomuldivass  21798  grpopnpcan2  21802  grponpncan  21804  grpodiveq  21805  ablomuldiv  21838  ablodivdiv4  21840  nvadd12  22063  nvmdi  22092  nvsubadd  22097  nvmtri2  22122  dipdi  22305  dipsubdir  22310  dipsubdi  22311  ax5seglem4  25783  cgr3tr4  25898  cgr3rflx  25900  seglemin  25959  linerflx1  25995  elicc3  26218  rngosubdi  26467  rngosubdir  26468  igenval2  26574  dmncan1  26584  mendlmod  27377  latmassOLD  29724  omlfh1N  29753  omlfh3N  29754  cvrnbtwn  29766  cvrnbtwn2  29770  cvrnbtwn4  29774  hlatj12  29865  cvrntr  29919  islpln2a  30042  3atnelvolN  30080  elpadd2at2  30301  paddasslem17  30330  paddass  30332  paddssw2  30338  pmapjlln1  30349  ltrn2ateq  30674  cdlemc3  30687  cdleme1b  30720  cdleme3b  30723  cdleme3c  30724  cdleme9b  30746  erngdvlem3  31484  erngdvlem3-rN  31492  dvalveclem  31520
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator