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

Theorem 3adant2r 1225
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 1201 . . 3  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
323adant1r 1223 . 2  |-  ( ( ( ps  /\  ta )  /\  ph  /\  ch )  ->  th )
433com12 1201 1  |-  ( (
ph  /\  ( ps  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 974
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 369  df-3an 976
This theorem is referenced by:  ltdiv23  10475  lediv23  10476  divalglem8  14265  isdrngd  17739  deg1tm  22809  ax5seglem1  24635  ax5seglem2  24636  nvaddsub4  25956  nmoub2i  26089  cdleme21at  33327  cdleme42f  33479  trlcoabs2N  33721  tendoplcl2  33777  tendopltp  33779  cdlemk2  33831  cdlemk8  33837  cdlemk9  33838  cdlemk9bN  33839  cdleml8  33982  dihglblem3N  34295  dihglblem3aN  34296  fourierdlem42  37280  lincscm  38523
  Copyright terms: Public domain W3C validator