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

Theorem 3adant3r 1182
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 1159 . . 3  |-  ( ( ch  /\  ps  /\  ph )  ->  th )
323adant1r 1178 . 2  |-  ( ( ( ch  /\  ta )  /\  ps  /\  ph )  ->  th )
433com13 1159 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  ta ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  cfeq0  8174  ltmul2  9899  lemul1  9900  lemul2  9901  lemuldiv  9927  lediv2  9938  ltdiv23  9939  lediv23  9940  dvdscmulr  12916  dvdsmulcr  12917  ndvdsadd  12966  rpexp12i  13160  isdrngd  15898  tsmsxp  18222  xblcntrps  18478  xblcntr  18479  gxnval  21886  gxneg  21892  gxnn0add  21900  gxnn0mul  21903  gxmul  21904  nvaddsub4  22180  hvmulcan2  22613  adjlnop  23627  wfrlem12  25584  frrlem11  25629  rrnmet  26580  mapfien2  27347  lfladd  30038  lflsub  30039  lshpset2N  30091  atcvrj1  30402  athgt  30427  ltrncnvel  31113  trlcnv  31136  trljat2  31138  cdlemc5  31166  trlcoabs  31692  trlcolem  31697  dicvaddcl  32162
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator