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

Theorem 3adant3r 1225
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 1201 . . 3  |-  ( ( ch  /\  ps  /\  ph )  ->  th )
323adant1r 1221 . 2  |-  ( ( ( ch  /\  ta )  /\  ps  /\  ph )  ->  th )
433com13 1201 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  ta ) )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  mapfien2  7868  cfeq0  8636  ltmul2  10393  lemul1  10394  lemul2  10395  lemuldiv  10424  lediv2  10435  ltdiv23  10436  lediv23  10437  dvdscmulr  13873  dvdsmulcr  13874  ndvdsadd  13925  rpexp12i  14122  isdrngd  17221  cramerimp  18983  tsmsxp  20420  xblcntrps  20676  xblcntr  20677  rrxmet  21598  gxnval  24966  gxneg  24972  gxnn0add  24980  gxnn0mul  24983  gxmul  24984  nvaddsub4  25260  hvmulcan2  25694  adjlnop  26709  wfrlem12  28959  frrlem11  29004  rrnmet  29956  mapfien2OLD  30674  fourierdlem42  31477  lincext3  32156  lfladd  33881  lflsub  33882  lshpset2N  33934  atcvrj1  34245  athgt  34270  ltrncnvel  34956  trlcnv  34979  trljat2  34981  cdlemc5  35009  trlcoabs  35535  trlcolem  35540  dicvaddcl  36005
  Copyright terms: Public domain W3C validator