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

Theorem 3adant3r3 1226
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 1216 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr3 1175 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    /\ w3a 991
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 190  df-an 377  df-3an 993
This theorem is referenced by:  ressress  15242  plttr  16271  plelttr  16273  latledi  16390  latmlej11  16391  latmlej21  16393  latmlej22  16394  latjass  16396  latj12  16397  latj31  16400  ipopos  16461  latdisdlem  16490  imasmnd2  16628  imasmnd  16629  grpaddsubass  16799  grpsubsub4  16802  grpnpncan  16804  imasgrp2  16856  imasgrp  16857  frgp0  17465  cmn12  17505  abladdsub  17512  imasring  17902  dvrass  17973  lss1  18217  islmhm2  18316  psrgrp  18677  psrlmod  18680  zntoslem  19182  ipdir  19261  t1sep  20441  mettri2  21411  xmetrtri  21425  xmetrtri2  21426  pi1grplem  22135  dchrabl  24238  motgrp  24644  xmstrkgc  24972  ax5seglem4  25018  grpomuldivass  26033  grpopnpcan2  26037  grponpncan  26039  grpodiveq  26040  ablomuldiv  26073  ablodivdiv4  26075  nvadd12  26298  nvmdi  26327  nvsubadd  26332  nvmtri2  26357  dipdi  26540  dipsubdir  26545  dipsubdi  26546  cgr3tr4  30869  cgr3rflx  30871  seglemin  30930  linerflx1  30966  elicc3  31023  rngosubdi  32238  rngosubdir  32239  igenval2  32345  dmncan1  32355  latmassOLD  32841  omlfh1N  32870  omlfh3N  32871  cvrnbtwn  32883  cvrnbtwn2  32887  cvrnbtwn4  32891  hlatj12  32982  cvrntr  33036  islpln2a  33159  3atnelvolN  33197  elpadd2at2  33418  paddasslem17  33447  paddass  33449  paddssw2  33455  pmapjlln1  33466  ltrn2ateq  33792  cdlemc3  33805  cdleme1b  33838  cdleme3b  33841  cdleme3c  33842  cdleme9b  33864  erngdvlem3  34603  erngdvlem3-rN  34611  dvalveclem  34639  mendlmod  36105  lincsumscmcl  40595
  Copyright terms: Public domain W3C validator