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

Theorem 3adant2r 1177
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 1155 . . 3  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
323adant1r 1175 . 2  |-  ( ( ( ps  /\  ta )  /\  ph  /\  ch )  ->  th )
433com12 1155 1  |-  ( (
ph  /\  ( ps  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ltdiv23  9692  lediv23  9693  divalglem8  12646  isdrngd  15586  deg1tm  19557  nvaddsub4  21274  nmoub2i  21407  ax5seglem1  24942  ax5seglem2  24943  cdleme21at  30335  cdleme42f  30487  trlcoabs2N  30729  tendoplcl2  30785  tendopltp  30787  cdlemk2  30839  cdlemk8  30845  cdlemk9  30846  cdlemk9bN  30847  cdleml8  30990  dihglblem3N  31303  dihglblem3aN  31304
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator