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

Theorem 3adant3r1 1214
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 1206 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr1 1164 1  |-  ( (
ph  /\  ( ta  /\ 
ps  /\  ch )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  plttr  16159  pltletr  16160  latjlej1  16254  latjlej2  16255  latnlej  16257  latnlej2  16260  latmlem2  16271  latledi  16278  latjass  16284  latj32  16286  latj13  16287  ipopos  16349  tsrlemax  16409  imasmnd2  16516  grpsubsub  16686  grpnnncan2  16694  mulgnn0ass  16730  mulgsubdir  16732  imasgrp2  16744  cmn32  17391  ablsubadd  17397  imasring  17790  zntoslem  19069  xmettri3  21310  mettri3  21311  xmetrtri  21312  xmetrtri2  21313  metrtri  21314  cphdivcl  22102  cphassr  22131  relogbmulexp  23657  grpodivdiv  25918  grpomuldivass  25919  grpopnpcan2  25923  grponnncan2  25924  ablo32  25956  ablodivdiv4  25961  ablodiv32  25962  ablonnncan  25963  nvmdi  26213  nvsubsub23  26225  nvmtri2  26243  dipdi  26426  dipassr  26429  dipsubdir  26431  dipsubdi  26432  dvrcan5  28508  cgr3tr4  30768  cgr3rflx  30770  endofsegid  30801  seglemin  30829  broutsideof2  30838  rngosubdi  32099  rngosubdir  32100  isdrngo2  32104  crngm23  32142  dmncan2  32217  latmassOLD  32707  latm32  32709  cvrnbtwn4  32757  cvrcmp2  32762  ltcvrntr  32901  atcvrj0  32905  3dim3  32946  paddasslem17  33313  paddass  33315  lautlt  33568  lautcvr  33569  lautj  33570  lautm  33571  erngdvlem3  34469  dvalveclem  34505  mendlmod  35972
  Copyright terms: Public domain W3C validator