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

Theorem 3adant3r1 1196
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 1188 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr1 1147 1  |-  ( (
ph  /\  ( ta  /\ 
ps  /\  ch )
)  ->  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:  plttr  15132  pltletr  15133  latjlej1  15227  latjlej2  15228  latnlej  15230  latnlej2  15233  latmlem2  15244  latledi  15251  latjass  15257  latj32  15259  latj13  15260  ipopos  15322  tsrlemax  15382  imasmnd2  15450  grpsubsub  15605  grpnnncan2  15612  mulgnn0ass  15647  mulgsubdir  15649  imasgrp2  15661  cmn32  16286  ablsubadd  16292  imasrng  16699  zntoslem  17964  xmettri3  19903  mettri3  19904  xmetrtri  19905  xmetrtri2  19906  metrtri  19907  cphdivcl  20676  cphassr  20705  grpodivdiv  23686  grpomuldivass  23687  grpopnpcan2  23691  grponnncan2  23692  ablo32  23724  ablodivdiv4  23729  ablodiv32  23730  ablonnncan  23731  nvmdi  23981  nvsubsub23  23993  nvmtri2  24011  dipdi  24194  dipassr  24197  dipsubdir  24199  dipsubdi  24200  dvrcan5  26212  cgr3tr4  28034  cgr3rflx  28036  endofsegid  28067  seglemin  28095  broutsideof2  28104  rngosubdi  28712  rngosubdir  28713  isdrngo2  28717  crngm23  28755  dmncan2  28830  mendlmod  29503  latmassOLD  32714  latm32  32716  cvrnbtwn4  32764  cvrcmp2  32769  ltcvrntr  32908  atcvrj0  32912  3dim3  32953  paddasslem17  33320  paddass  33322  lautlt  33575  lautcvr  33576  lautj  33577  lautm  33578  erngdvlem3  34474  dvalveclem  34510
  Copyright terms: Public domain W3C validator