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

Theorem 3adant3r 1179
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 1156 . . 3  |-  ( ( ch  /\  ps  /\  ph )  ->  th )
323adant1r 1175 . 2  |-  ( ( ( ch  /\  ta )  /\  ps  /\  ph )  ->  th )
433com13 1156 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  ta ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  cfeq0  7898  ltmul2  9623  lemul1  9624  lemul2  9625  lemuldiv  9651  lediv2  9662  ltdiv23  9663  lediv23  9664  dvdscmulr  12573  dvdsmulcr  12574  ndvdsadd  12623  rpexp12i  12817  isdrngd  15553  tsmsxp  17853  xblcntr  17979  gxnval  20943  gxneg  20949  gxnn0add  20957  gxnn0mul  20960  gxmul  20961  nvaddsub4  21235  hvmulcan2  21668  adjlnop  22682  wfrlem12  24338  frrlem11  24364  itg2addnc  25005  prjmapcp2  25273  valvalcurfn  25309  conttnf2  25665  distmlva  25791  rrnmet  26656  mapfien2  27361  lfladd  29878  lflsub  29879  lshpset2N  29931  atcvrj1  30242  athgt  30267  ltrncnvel  30953  trlcnv  30976  trljat2  30978  cdlemc5  31006  trlcoabs  31532  trlcolem  31537  dicvaddcl  32002
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