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

Theorem 3ad2antl3 1147
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
Hypothesis
Ref Expression
3ad2antl.1  |-  ( (
ph  /\  ch )  ->  th )
Assertion
Ref Expression
3ad2antl3  |-  ( ( ( ps  /\  ta  /\ 
ph )  /\  ch )  ->  th )

Proof of Theorem 3ad2antl3
StepHypRef Expression
1 3ad2antl.1 . . 3  |-  ( (
ph  /\  ch )  ->  th )
21adantll 708 . 2  |-  ( ( ( ta  /\  ph )  /\  ch )  ->  th )
323adantl1 1139 1  |-  ( ( ( ps  /\  ta  /\ 
ph )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 960
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 962
This theorem is referenced by:  rspc3ev  3074  brcogw  4997  fnsuppresOLD  5927  cocan1  5984  ov6g  6219  dif1enOLD  7534  dif1en  7535  cfsmolem  8429  coftr  8432  axcc3  8597  axdc4lem  8614  gruf  8968  dedekindle  9524  zdivmul  10704  coprmdvds  13773  lubss  15276  gsumccat  15501  odeq  16035  ghmplusg  16310  lmhmvsca  17050  islindf4  18111  mndifsplit  18286  gsummatr01lem3  18307  gsummatr01  18309  elcls  18521  cnpresti  18736  cmpsublem  18846  ptpjcn  19028  elfm3  19367  rnelfmlem  19369  nmoix  20152  ig1pdvds  21535  coeid3  21595  amgm  22271  brbtwn2  22976  colinearalg  22981  axsegconlem1  22988  ax5seglem1  22999  ax5seglem2  23000  usgra2edg  23126  homco1  25030  hoadddi  25032  br6  27416  bpolycl  28044  comppfsc  28425  upixp  28469  filbcmb  28480  mzprename  28933  infmrgelbi  29066  stoweidlem17  29660  stoweidlem28  29671  clwwlkel  30303  clwwisshclww  30319  3dim1  32724  llni  32765  lplni  32789  lvoli  32832  cdleme42mgN  33745
  Copyright terms: Public domain W3C validator