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

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

Proof of Theorem 3adant3r1
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213expb 1197 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr1 1155 1  |-  ( (
ph  /\  ( ta  /\ 
ps  /\  ch )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  plttr  15456  pltletr  15457  latjlej1  15551  latjlej2  15552  latnlej  15554  latnlej2  15557  latmlem2  15568  latledi  15575  latjass  15581  latj32  15583  latj13  15584  ipopos  15646  tsrlemax  15706  imasmnd2  15775  grpsubsub  15934  grpnnncan2  15942  mulgnn0ass  15978  mulgsubdir  15980  imasgrp2  15992  cmn32  16619  ablsubadd  16625  imasrng  17064  zntoslem  18378  xmettri3  20607  mettri3  20608  xmetrtri  20609  xmetrtri2  20610  metrtri  20611  cphdivcl  21380  cphassr  21409  grpodivdiv  24942  grpomuldivass  24943  grpopnpcan2  24947  grponnncan2  24948  ablo32  24980  ablodivdiv4  24985  ablodiv32  24986  ablonnncan  24987  nvmdi  25237  nvsubsub23  25249  nvmtri2  25267  dipdi  25450  dipassr  25453  dipsubdir  25455  dipsubdi  25456  dvrcan5  27462  cgr3tr4  29295  cgr3rflx  29297  endofsegid  29328  seglemin  29356  broutsideof2  29365  rngosubdi  29975  rngosubdir  29976  isdrngo2  29980  crngm23  30018  dmncan2  30093  mendlmod  30763  latmassOLD  34035  latm32  34037  cvrnbtwn4  34085  cvrcmp2  34090  ltcvrntr  34229  atcvrj0  34233  3dim3  34274  paddasslem17  34641  paddass  34643  lautlt  34896  lautcvr  34897  lautj  34898  lautm  34899  erngdvlem3  35795  dvalveclem  35831
  Copyright terms: Public domain W3C validator