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

Theorem 3adant3r1 1197
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 1189 . 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  15262  pltletr  15263  latjlej1  15357  latjlej2  15358  latnlej  15360  latnlej2  15363  latmlem2  15374  latledi  15381  latjass  15387  latj32  15389  latj13  15390  ipopos  15452  tsrlemax  15512  imasmnd2  15580  grpsubsub  15736  grpnnncan2  15743  mulgnn0ass  15778  mulgsubdir  15780  imasgrp2  15792  cmn32  16419  ablsubadd  16425  imasrng  16837  zntoslem  18117  xmettri3  20063  mettri3  20064  xmetrtri  20065  xmetrtri2  20066  metrtri  20067  cphdivcl  20836  cphassr  20865  grpodivdiv  23907  grpomuldivass  23908  grpopnpcan2  23912  grponnncan2  23913  ablo32  23945  ablodivdiv4  23950  ablodiv32  23951  ablonnncan  23952  nvmdi  24202  nvsubsub23  24214  nvmtri2  24232  dipdi  24415  dipassr  24418  dipsubdir  24420  dipsubdi  24421  dvrcan5  26426  cgr3tr4  28247  cgr3rflx  28249  endofsegid  28280  seglemin  28308  broutsideof2  28317  rngosubdi  28927  rngosubdir  28928  isdrngo2  28932  crngm23  28970  dmncan2  29045  mendlmod  29718  latmassOLD  33232  latm32  33234  cvrnbtwn4  33282  cvrcmp2  33287  ltcvrntr  33426  atcvrj0  33430  3dim3  33471  paddasslem17  33838  paddass  33840  lautlt  34093  lautcvr  34094  lautj  34095  lautm  34096  erngdvlem3  34992  dvalveclem  35028
  Copyright terms: Public domain W3C validator