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

Theorem 3adant3r 1181
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
3adant3r  |-  ( (
ph  /\  ps  /\  ( ch  /\  ta ) )  ->  th )

Proof of Theorem 3adant3r
StepHypRef Expression
1 3adant1l.1 . . . 4  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213com13 1158 . . 3  |-  ( ( ch  /\  ps  /\  ph )  ->  th )
323adant1r 1177 . 2  |-  ( ( ( ch  /\  ta )  /\  ps  /\  ph )  ->  th )
433com13 1158 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  ta ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  cfeq0  8120  ltmul2  9845  lemul1  9846  lemul2  9847  lemuldiv  9873  lediv2  9884  ltdiv23  9885  lediv23  9886  dvdscmulr  12861  dvdsmulcr  12862  ndvdsadd  12911  rpexp12i  13105  isdrngd  15843  tsmsxp  18167  xblcntrps  18423  xblcntr  18424  gxnval  21831  gxneg  21837  gxnn0add  21845  gxnn0mul  21848  gxmul  21849  nvaddsub4  22125  hvmulcan2  22558  adjlnop  23572  wfrlem12  25517  frrlem11  25543  rrnmet  26470  mapfien2  27168  lfladd  29595  lflsub  29596  lshpset2N  29648  atcvrj1  29959  athgt  29984  ltrncnvel  30670  trlcnv  30693  trljat2  30695  cdlemc5  30723  trlcoabs  31249  trlcolem  31254  dicvaddcl  31719
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator