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  8062  ltmul2  9786  lemul1  9787  lemul2  9788  lemuldiv  9814  lediv2  9825  ltdiv23  9826  lediv23  9827  dvdscmulr  12798  dvdsmulcr  12799  ndvdsadd  12848  rpexp12i  13042  isdrngd  15780  tsmsxp  18098  xblcntr  18330  gxnval  21689  gxneg  21695  gxnn0add  21703  gxnn0mul  21706  gxmul  21707  nvaddsub4  21983  hvmulcan2  22416  adjlnop  23430  wfrlem12  25284  frrlem11  25310  itg2addnc  25952  rrnmet  26222  mapfien2  26920  lfladd  29232  lflsub  29233  lshpset2N  29285  atcvrj1  29596  athgt  29621  ltrncnvel  30307  trlcnv  30330  trljat2  30332  cdlemc5  30360  trlcoabs  30886  trlcolem  30891  dicvaddcl  31356
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