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  6777  gxneg  20949  gxnn0add  20957  gxsub  20959  nvaddsub4  21235  adjlnop  22682  wfrlem12  24338  frrlem11  24364  mulinvsca  25583  distmlva  25791  distsava  25792  rrnmet  26656  lflsub  29879  lflmul  29880  cvlatexch3  30150  cdleme5  31051  cdlemeg46rjgN  31333  cdlemg2l  31414  cdlemg10c  31450  tendospcanN  31835  dicvaddcl  32002  dicvscacl  32003  dochexmidlem8  32279
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