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

Theorem 3adant3r3 1198
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 1188 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr3 1149 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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  df-3an 967
This theorem is referenced by:  ressress  14250  plttr  15155  plelttr  15157  latledi  15274  latmlej11  15275  latmlej21  15277  latmlej22  15278  latjass  15280  latj12  15281  latj31  15284  ipopos  15345  latdisdlem  15374  ismndd  15459  imasmnd2  15473  imasmnd  15474  grpaddsubass  15630  grpsubsub4  15633  grpnpncan  15635  imasgrp2  15685  imasgrp  15686  frgp0  16272  cmn12  16312  abladdsub  16319  imasrng  16726  dvrass  16797  lss1  17035  islmhm2  17134  psrgrp  17484  psrlmod  17487  zntoslem  18004  ipdir  18083  t1sep  18989  mettri2  19931  xmetrtri  19945  xmetrtri2  19946  pi1grplem  20636  dchrabl  22608  ax5seglem4  23193  grpomuldivass  23751  grpopnpcan2  23755  grponpncan  23757  grpodiveq  23758  ablomuldiv  23791  ablodivdiv4  23793  nvadd12  24016  nvmdi  24045  nvsubadd  24050  nvmtri2  24075  dipdi  24258  dipsubdir  24263  dipsubdi  24264  cgr3tr4  28098  cgr3rflx  28100  seglemin  28159  linerflx1  28195  elicc3  28531  rngosubdi  28778  rngosubdir  28779  igenval2  28885  dmncan1  28895  mendlmod  29569  lincsumscmcl  30986  latmassOLD  32893  omlfh1N  32922  omlfh3N  32923  cvrnbtwn  32935  cvrnbtwn2  32939  cvrnbtwn4  32943  hlatj12  33034  cvrntr  33088  islpln2a  33211  3atnelvolN  33249  elpadd2at2  33470  paddasslem17  33499  paddass  33501  paddssw2  33507  pmapjlln1  33518  ltrn2ateq  33843  cdlemc3  33856  cdleme1b  33889  cdleme3b  33892  cdleme3c  33893  cdleme9b  33915  erngdvlem3  34653  erngdvlem3-rN  34661  dvalveclem  34689
  Copyright terms: Public domain W3C validator