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

Theorem 3adant3l 1181
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 1159 . . 3  |-  ( ( ch  /\  ps  /\  ph )  ->  th )
323adant1l 1177 . 2  |-  ( ( ( ta  /\  ch )  /\  ps  /\  ph )  ->  th )
433com13 1159 1  |-  ( (
ph  /\  ps  /\  ( ta  /\  ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  ecopovtrn  7009  gxneg  21856  gxnn0add  21864  gxsub  21866  nvaddsub4  22144  adjlnop  23591  wfrlem12  25551  frrlem11  25596  rrnmet  26540  lflsub  29927  lflmul  29928  cvlatexch3  30198  cdleme5  31099  cdlemeg46rjgN  31381  cdlemg2l  31462  cdlemg10c  31498  tendospcanN  31883  dicvaddcl  32050  dicvscacl  32051  dochexmidlem8  32327
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator