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

Theorem 3adant3r 1261
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 1210 . . 3  |-  ( ( ch  /\  ps  /\  ph )  ->  th )
323adant1r 1257 . 2  |-  ( ( ( ch  /\  ta )  /\  ps  /\  ph )  ->  th )
433com13 1210 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  ta ) )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  wfrlem12  7046  mapfien2  7919  cfeq0  8675  ltmul2  10445  lemul1  10446  lemul2  10447  lemuldiv  10475  lediv2  10485  ltdiv23  10486  lediv23  10487  dvdscmulr  14298  dvdsmulcr  14299  ndvdsadd  14353  rpexp12i  14634  isdrngd  17928  cramerimp  19635  tsmsxp  21093  xblcntrps  21349  xblcntr  21350  rrxmet  22248  gxnval  25830  gxneg  25836  gxnn0add  25844  gxnn0mul  25847  gxmul  25848  nvaddsub4  26124  hvmulcan2  26558  adjlnop  27571  frrlem11  30310  rrnmet  31865  lfladd  32341  lflsub  32342  lshpset2N  32394  atcvrj1  32705  athgt  32730  ltrncnvel  33416  trlcnv  33440  trljat2  33442  cdlemc5  33470  trlcoabs  33997  trlcolem  34002  dicvaddcl  34467  fourierdlem42  37584  lincext3  39022
  Copyright terms: Public domain W3C validator