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

Theorem 3adant2r 1179
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
3adant2r  |-  ( (
ph  /\  ( ps  /\ 
ta )  /\  ch )  ->  th )

Proof of Theorem 3adant2r
StepHypRef Expression
1 3adant1l.1 . . . 4  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213com12 1157 . . 3  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
323adant1r 1177 . 2  |-  ( ( ( ps  /\  ta )  /\  ph  /\  ch )  ->  th )
433com12 1157 1  |-  ( (
ph  /\  ( ps  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  ltdiv23  9901  lediv23  9902  divalglem8  12920  isdrngd  15860  deg1tm  20041  nvaddsub4  22142  nmoub2i  22275  ax5seglem1  25867  ax5seglem2  25868  cdleme21at  31125  cdleme42f  31277  trlcoabs2N  31519  tendoplcl2  31575  tendopltp  31577  cdlemk2  31629  cdlemk8  31635  cdlemk9  31636  cdlemk9bN  31637  cdleml8  31780  dihglblem3N  32093  dihglblem3aN  32094
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator