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

Theorem 3adant3l 1178
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
3adant1l.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3adant3l  |-  ( (
ph  /\  ps  /\  ( ta  /\  ch ) )  ->  th )

Proof of Theorem 3adant3l
StepHypRef Expression
1 3adant1l.1 . . . 4  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213com13 1156 . . 3  |-  ( ( ch  /\  ps  /\  ph )  ->  th )
323adant1l 1174 . 2  |-  ( ( ( ta  /\  ch )  /\  ps  /\  ph )  ->  th )
433com13 1156 1  |-  ( (
ph  /\  ps  /\  ( ta  /\  ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ecopovtrn  6761  gxneg  20933  gxnn0add  20941  gxsub  20943  nvaddsub4  21219  adjlnop  22666  wfrlem12  24267  frrlem11  24293  mulinvsca  25480  distmlva  25688  distsava  25689  rrnmet  26553  lflsub  29257  lflmul  29258  cvlatexch3  29528  cdleme5  30429  cdlemeg46rjgN  30711  cdlemg2l  30792  cdlemg10c  30828  tendospcanN  31213  dicvaddcl  31380  dicvscacl  31381  dochexmidlem8  31657
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