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

Theorem 3adant3l 1226
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 1202 . . 3  |-  ( ( ch  /\  ps  /\  ph )  ->  th )
323adant1l 1222 . 2  |-  ( ( ( ta  /\  ch )  /\  ps  /\  ph )  ->  th )
433com13 1202 1  |-  ( (
ph  /\  ps  /\  ( ta  /\  ch ) )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 974
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 369  df-3an 976
This theorem is referenced by:  wfrlem12  7031  ecopovtrn  7450  rrxmet  22125  gxneg  25668  gxnn0add  25676  gxsub  25678  nvaddsub4  25956  adjlnop  27404  pl1cn  28376  frrlem11  30086  rrnmet  31587  lflsub  32065  lflmul  32066  cvlatexch3  32336  cdleme5  33238  cdlemeg46rjgN  33521  cdlemg2l  33602  cdlemg10c  33638  tendospcanN  34023  dicvaddcl  34190  dicvscacl  34191  dochexmidlem8  34467  fourierdlem42  37280  fourierdlem113  37351
  Copyright terms: Public domain W3C validator