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

Theorem 3adant2r 1180
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 1158 . . 3  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
323adant1r 1178 . 2  |-  ( ( ( ps  /\  ta )  /\  ph  /\  ch )  ->  th )
433com12 1158 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:  ltdiv23  9902  lediv23  9903  divalglem8  12921  isdrngd  15861  deg1tm  20042  nvaddsub4  22143  nmoub2i  22276  ax5seglem1  25868  ax5seglem2  25869  cdleme21at  31126  cdleme42f  31278  trlcoabs2N  31520  tendoplcl2  31576  tendopltp  31578  cdlemk2  31630  cdlemk8  31636  cdlemk9  31637  cdlemk9bN  31638  cdleml8  31781  dihglblem3N  32094  dihglblem3aN  32095
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