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

Theorem 3adant2r 1213
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 1191 . . 3  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
323adant1r 1211 . 2  |-  ( ( ( ps  /\  ta )  /\  ph  /\  ch )  ->  th )
433com12 1191 1  |-  ( (
ph  /\  ( ps  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  ltdiv23  10222  lediv23  10223  divalglem8  13603  isdrngd  16856  deg1tm  21589  ax5seglem1  23173  ax5seglem2  23174  nvaddsub4  24040  nmoub2i  24173  lincscm  30962  cdleme21at  33970  cdleme42f  34122  trlcoabs2N  34364  tendoplcl2  34420  tendopltp  34422  cdlemk2  34474  cdlemk8  34480  cdlemk9  34481  cdlemk9bN  34482  cdleml8  34625  dihglblem3N  34938  dihglblem3aN  34939
  Copyright terms: Public domain W3C validator