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  7882  ltmul2  9607  lemul1  9608  lemul2  9609  lemuldiv  9635  lediv2  9646  ltdiv23  9647  lediv23  9648  dvdscmulr  12557  dvdsmulcr  12558  ndvdsadd  12607  rpexp12i  12801  isdrngd  15537  tsmsxp  17837  xblcntr  17963  gxnval  20927  gxneg  20933  gxnn0add  20941  gxnn0mul  20944  gxmul  20945  nvaddsub4  21219  hvmulcan2  21652  adjlnop  22666  wfrlem12  24267  frrlem11  24293  prjmapcp2  25170  valvalcurfn  25206  conttnf2  25562  distmlva  25688  rrnmet  26553  mapfien2  27258  lfladd  29256  lflsub  29257  lshpset2N  29309  atcvrj1  29620  athgt  29645  ltrncnvel  30331  trlcnv  30354  trljat2  30356  cdlemc5  30384  trlcoabs  30910  trlcolem  30915  dicvaddcl  31380
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