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

Theorem 3adant3l 1224
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 1201 . . 3  |-  ( ( ch  /\  ps  /\  ph )  ->  th )
323adant1l 1220 . 2  |-  ( ( ( ta  /\  ch )  /\  ps  /\  ph )  ->  th )
433com13 1201 1  |-  ( (
ph  /\  ps  /\  ( ta  /\  ch ) )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  ecopovtrn  7411  rrxmet  21570  gxneg  24944  gxnn0add  24952  gxsub  24954  nvaddsub4  25232  adjlnop  26681  pl1cn  27573  wfrlem12  28931  frrlem11  28976  rrnmet  29928  fourierdlem42  31449  fourierdlem113  31520  lflsub  33864  lflmul  33865  cvlatexch3  34135  cdleme5  35036  cdlemeg46rjgN  35318  cdlemg2l  35399  cdlemg10c  35435  tendospcanN  35820  dicvaddcl  35987  dicvscacl  35988  dochexmidlem8  36264
  Copyright terms: Public domain W3C validator