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  9647  lediv23  9648  divalglem8  12599  isdrngd  15537  deg1tm  19504  nvaddsub4  21219  nmoub2i  21352  ax5seglem1  24556  ax5seglem2  24557  cdleme21at  30517  cdleme42f  30669  trlcoabs2N  30911  tendoplcl2  30967  tendopltp  30969  cdlemk2  31021  cdlemk8  31027  cdlemk9  31028  cdlemk9bN  31029  cdleml8  31172  dihglblem3N  31485  dihglblem3aN  31486
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