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

Theorem 3adant3r 1215
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 1192 . . 3  |-  ( ( ch  /\  ps  /\  ph )  ->  th )
323adant1r 1211 . 2  |-  ( ( ( ch  /\  ta )  /\  ps  /\  ph )  ->  th )
433com13 1192 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  ta ) )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  mapfien2  7656  cfeq0  8423  ltmul2  10178  lemul1  10179  lemul2  10180  lemuldiv  10209  lediv2  10220  ltdiv23  10221  lediv23  10222  dvdscmulr  13559  dvdsmulcr  13560  ndvdsadd  13610  rpexp12i  13806  isdrngd  16855  cramerimp  18490  tsmsxp  19727  xblcntrps  19983  xblcntr  19984  rrxmet  20905  gxnval  23745  gxneg  23751  gxnn0add  23759  gxnn0mul  23762  gxmul  23763  nvaddsub4  24039  hvmulcan2  24473  adjlnop  25488  wfrlem12  27733  frrlem11  27778  rrnmet  28725  mapfien2OLD  29446  lincext3  30987  lfladd  32708  lflsub  32709  lshpset2N  32761  atcvrj1  33072  athgt  33097  ltrncnvel  33783  trlcnv  33806  trljat2  33808  cdlemc5  33836  trlcoabs  34362  trlcolem  34367  dicvaddcl  34832
  Copyright terms: Public domain W3C validator