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

Theorem 3adant3r1 1160
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 1152 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr1 1114 1  |-  ( (
ph  /\  ( ta  /\ 
ps  /\  ch )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  plttr  14120  pltletr  14121  joinle  14143  latjlej1  14187  latjlej2  14188  latnlej  14190  latnlej2  14193  latmlem2  14204  latledi  14211  latjass  14217  latj32  14219  latj13  14220  ipopos  14279  tsrlemax  14345  imasmnd2  14425  grpsubsub  14570  grpnnncan2  14577  mulgnn0ass  14612  mulgsubdir  14614  imasgrp2  14626  cmn32  15123  ablsubadd  15129  imasrng  15418  zntoslem  16526  xmettri3  17933  mettri3  17934  xmetrtri  17935  xmetrtri2  17936  metrtri  17937  cphdivcl  18634  cphassr  18663  grpodivdiv  20931  grpomuldivass  20932  grpopnpcan2  20936  grponnncan2  20937  ablo32  20969  ablodivdiv4  20974  ablodiv32  20975  ablonnncan  20976  nvmdi  21224  nvsubsub23  21236  nvmtri2  21254  dipdi  21437  dipassr  21440  dipsubdir  21442  dipsubdi  21443  cgr3tr4  24747  cgr3rflx  24749  endofsegid  24780  seglemin  24808  broutsideof2  24817  grpodrcan  25478  dblsubvec  25577  mvecrtol2  25580  addassv  25759  cmpassoh  25904  homgrf  25905  rngosubdi  26687  rngosubdir  26688  isdrngo2  26692  crngm23  26730  dmncan2  26805  mendlmod  27604  latmassOLD  30041  latm32  30043  cvrnbtwn4  30091  cvrcmp2  30096  ltcvrntr  30235  atcvrj0  30239  3dim3  30280  paddasslem17  30647  paddass  30649  lautlt  30902  lautcvr  30903  lautj  30904  lautm  30905  erngdvlem3  31801  dvalveclem  31837
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator