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  9663  lediv23  9664  divalglem8  12615  isdrngd  15553  deg1tm  19520  nvaddsub4  21235  nmoub2i  21368  ax5seglem1  24628  ax5seglem2  24629  cdleme21at  31139  cdleme42f  31291  trlcoabs2N  31533  tendoplcl2  31589  tendopltp  31591  cdlemk2  31643  cdlemk8  31649  cdlemk9  31650  cdlemk9bN  31651  cdleml8  31794  dihglblem3N  32107  dihglblem3aN  32108
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