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

Theorem 3adant2r 1218
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 1195 . . 3  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
323adant1r 1216 . 2  |-  ( ( ( ps  /\  ta )  /\  ph  /\  ch )  ->  th )
433com12 1195 1  |-  ( (
ph  /\  ( ps  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 968
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 371  df-3an 970
This theorem is referenced by:  ltdiv23  10427  lediv23  10428  divalglem8  13908  isdrngd  17199  deg1tm  22249  ax5seglem1  23902  ax5seglem2  23903  nvaddsub4  25220  nmoub2i  25353  fourierdlem42  31406  lincscm  31981  cdleme21at  35001  cdleme42f  35153  trlcoabs2N  35395  tendoplcl2  35451  tendopltp  35453  cdlemk2  35505  cdlemk8  35511  cdlemk9  35512  cdlemk9bN  35513  cdleml8  35656  dihglblem3N  35969  dihglblem3aN  35970
  Copyright terms: Public domain W3C validator