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

Theorem 3adant3r1 1162
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 1154 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr1 1116 1  |-  ( (
ph  /\  ( ta  /\ 
ps  /\  ch )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  plttr  14427  pltletr  14428  joinle  14450  latjlej1  14494  latjlej2  14495  latnlej  14497  latnlej2  14500  latmlem2  14511  latledi  14518  latjass  14524  latj32  14526  latj13  14527  ipopos  14586  tsrlemax  14652  imasmnd2  14732  grpsubsub  14877  grpnnncan2  14884  mulgnn0ass  14919  mulgsubdir  14921  imasgrp2  14933  cmn32  15430  ablsubadd  15436  imasrng  15725  zntoslem  16837  xmettri3  18383  mettri3  18384  xmetrtri  18385  xmetrtri2  18386  metrtri  18387  cphdivcl  19145  cphassr  19174  grpodivdiv  21836  grpomuldivass  21837  grpopnpcan2  21841  grponnncan2  21842  ablo32  21874  ablodivdiv4  21879  ablodiv32  21880  ablonnncan  21881  nvmdi  22131  nvsubsub23  22143  nvmtri2  22161  dipdi  22344  dipassr  22347  dipsubdir  22349  dipsubdi  22350  dvrcan5  24229  cgr3tr4  25986  cgr3rflx  25988  endofsegid  26019  seglemin  26047  broutsideof2  26056  rngosubdi  26569  rngosubdir  26570  isdrngo2  26574  crngm23  26612  dmncan2  26687  mendlmod  27478  latmassOLD  30027  latm32  30029  cvrnbtwn4  30077  cvrcmp2  30082  ltcvrntr  30221  atcvrj0  30225  3dim3  30266  paddasslem17  30633  paddass  30635  lautlt  30888  lautcvr  30889  lautj  30890  lautm  30891  erngdvlem3  31787  dvalveclem  31823
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